Skip to content

remove a simp lemma and swap an equality #254

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
teorth merged 1 commit into from
Jul 31, 2025
Merged

remove a simp lemma and swap an equality #254

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions analysis/Analysis/Section_11_2.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -118,7 +118,7 @@ example : PiecewiseConstantOn f_11_2_4 (Icc 1 6) := by
sorry

/-- Example 11.2.6 -/
theorem PiecewiseConstantOn.of_const {f:ℝ → ℝ} {I: BoundedInterval} (h: ConstantOn f (I:Set ℝ)) :
theorem ConstantOn.piecewiseConstantOn {f:ℝ → ℝ} {I: BoundedInterval} (h: ConstantOn f (I:Set ℝ)) :
PiecewiseConstantOn f I := by sorry

/-- Lemma 11.2.7 / Exercise 11.2.1 -/
Expand Down Expand Up @@ -166,7 +166,7 @@ noncomputable abbrev PiecewiseConstantWith.integ (f:ℝ → ℝ) {I: BoundedInte
ℝ := ∑ J ∈ P.intervals, constant_value_on f (J:Set ℝ) * |J|ₗ

theorem PiecewiseConstantWith.integ_congr {f g:ℝ → ℝ} {I: BoundedInterval} {P: Partition I}
(h: ∀ x ∈ (I:Set ℝ), f x = g x) : PiecewiseConstantWith.integ f P = PiecewiseConstantWith.integ g P := by
(h: ∀ x ∈ (I:Set ℝ), f x = g x) : integ f P = integ g P := by
simp only [integ, Subtype.forall]
apply Finset.sum_congr rfl; intro J hJ; congr 1; apply constant_value_on_congr; intros
have := P.contains _ hJ; rw [subset_iff] at this
Expand Down Expand Up @@ -222,7 +222,7 @@ theorem PiecewiseConstantOn.integ_def {f:ℝ → ℝ} {I: BoundedInterval} {P: P
simp [integ, h']; exact PiecewiseConstantWith.integ_eq h'.choose_spec h

theorem PiecewiseConstantOn.integ_congr {f g:ℝ → ℝ} {I: BoundedInterval}
(h: ∀ x ∈ (I:Set ℝ), f x = g x) : PiecewiseConstantOn.integ f I = PiecewiseConstantOn.integ g I := by
(h: ∀ x ∈ (I:Set ℝ), f x = g x) : integ f I = integ g I := by
by_cases hf : PiecewiseConstantOn f I
<;> have hg := hf <;> rw [congr h] at hg <;> simp [integ, hf, hg]
rw [PiecewiseConstantWith.integ_congr h, ←integ_def hg.choose_spec, ←integ_def ?_]
Expand Down
6 changes: 3 additions & 3 deletions analysis/Analysis/Section_11_3.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,13 +46,13 @@ lemma integral_bound_upper_of_bounded {f:ℝ → ℝ} {M:ℝ} {I: BoundedInterva
simp
refine ⟨ fun _ ↦ M , ⟨ ⟨ ?_, ?_, ⟩, PiecewiseConstantOn.integ_const M I ⟩ ⟩
. peel h with _ _ h'; simp [abs_le'] at h'; simp [h'.1]
exact PiecewiseConstantOn.of_const (ConstantOn.of_const (c := M) (by simp))
exact (ConstantOn.of_const (c := M) (by simp)).piecewiseConstantOn

lemma integral_bound_lower_of_bounded {f:ℝ → ℝ} {M:ℝ} {I: BoundedInterval} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M) : -M * |I|ₗ ∈ (fun g ↦ PiecewiseConstantOn.integ g I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I} := by
simp
refine ⟨ fun _ ↦ -M , ⟨ ⟨ ?_, ?_, ⟩, by convert PiecewiseConstantOn.integ_const (-M) I using 1; simp ⟩ ⟩
. peel h with _ _ h'; simp [abs_le'] at h'; simp; linarith
exact PiecewiseConstantOn.of_const (ConstantOn.of_const (c := -M) (by simp))
exact (ConstantOn.of_const (c := -M) (by simp)).piecewiseConstantOn

lemma integral_bound_upper_nonempty {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I) : ((fun g ↦ PiecewiseConstantOn.integ g I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty := by
obtain ⟨ _, h ⟩ := h; exact Set.nonempty_of_mem (integral_bound_upper_of_bounded h)
Expand Down Expand Up @@ -142,7 +142,7 @@ theorem integ_on_subsingleton {f:ℝ → ℝ} {I: BoundedInterval} (hI: |I|ₗ =
IntegrableOn f I ∧ integ f I = 0 := by
have _ := length_of_subsingleton.mpr hI
have hconst : ConstantOn f I := ConstantOn.of_subsingleton
convert integ_of_piecewise_const (PiecewiseConstantOn.of_const hconst)
convert integ_of_piecewise_const hconst.piecewiseConstantOn
simp [PiecewiseConstantOn.integ_const' hconst, hI]

/-- Definition 11.3.9 (Riemann sums). The restriction to positive length J is not needed thanks to various junk value conventions. -/
Expand Down
8 changes: 4 additions & 4 deletions analysis/Analysis/Section_11_4.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -186,7 +186,7 @@ theorem integ_of_mul_nonneg {I: BoundedInterval} {f g:ℝ → ℝ} (hf: Integrab
have : ∃ f', MinorizesOn f' f I ∧ PiecewiseConstantOn f' I ∧ integ f I - ε < PiecewiseConstantOn.integ f' I ∧ MajorizesOn f' 0 I := by
obtain ⟨ f', hf'min, hf'const, hf'int ⟩ := gt_of_lt_lower_integral hf.1 (show integ f I - ε < lower_integral f I by linarith)
use max f' 0
have hzero := PiecewiseConstantOn.of_const (ConstantOn.of_const' 0 I)
have hzero := (ConstantOn.of_const' 0 I).piecewiseConstantOn
and_intros
. peel hf_nonneg with x hx _; specialize hf'min _ hx; aesop
. exact hf'const.max hzero
Expand All @@ -196,7 +196,7 @@ theorem integ_of_mul_nonneg {I: BoundedInterval} {f g:ℝ → ℝ} (hf: Integrab
have : ∃ g', MinorizesOn g' g I ∧ PiecewiseConstantOn g' I ∧ integ g I - ε < PiecewiseConstantOn.integ g' I ∧ MajorizesOn g' 0 I := by
obtain ⟨ g', hg'min, hg'const, hg'int ⟩ := gt_of_lt_lower_integral hg.1 (show integ g I - ε < lower_integral g I by linarith)
use max g' 0
have hzero := PiecewiseConstantOn.of_const (ConstantOn.of_const' 0 I)
have hzero := (ConstantOn.of_const' 0 I).piecewiseConstantOn
and_intros
. peel hg_nonneg with x hx _; specialize hg'min _ hx; aesop
. exact hg'const.max hzero
Expand All @@ -206,7 +206,7 @@ theorem integ_of_mul_nonneg {I: BoundedInterval} {f g:ℝ → ℝ} (hf: Integrab
have : ∃ f'', MajorizesOn f'' f I ∧ PiecewiseConstantOn f'' I ∧ PiecewiseConstantOn.integ f'' I < integ f I + ε ∧ MinorizesOn f'' (fun _ ↦ M₁) I := by
obtain ⟨ f'', hf''maj, hf''const, hf''int ⟩ := lt_of_gt_upper_integral hf.1 (show upper_integral f I < integ f I + ε by linarith)
use min f'' (fun _ ↦ M₁)
have hM₁_piece := PiecewiseConstantOn.of_const (ConstantOn.of_const' M₁ I)
have hM₁_piece := (ConstantOn.of_const' M₁ I).piecewiseConstantOn
and_intros
. peel hM₁ with x hx hM₁; rw [abs_le'] at hM₁
specialize hf''maj _ hx; simp [hf''maj, hM₁.1]
Expand All @@ -218,7 +218,7 @@ theorem integ_of_mul_nonneg {I: BoundedInterval} {f g:ℝ → ℝ} (hf: Integrab
have : ∃ g'', MajorizesOn g'' g I ∧ PiecewiseConstantOn g'' I ∧ PiecewiseConstantOn.integ g'' I < integ g I + ε ∧ MinorizesOn g'' (fun _ ↦ M₂) I := by
obtain ⟨ g'', hg''maj, hg''const, hg''int ⟩ := lt_of_gt_upper_integral hg.1 (show upper_integral g I < integ g I + ε by linarith)
use min g'' (fun _ ↦ M₂)
have hM₂_piece := PiecewiseConstantOn.of_const (ConstantOn.of_const' M₂ I)
have hM₂_piece := (ConstantOn.of_const' M₂ I).piecewiseConstantOn
and_intros
. peel hM₂ with x hx hM₂; rw [abs_le'] at hM₂
specialize hg''maj _ hx; simp [hg''maj, hM₂.1]
Expand Down
8 changes: 4 additions & 4 deletions analysis/Analysis/Section_11_5.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -170,10 +170,10 @@ theorem integ_of_bdd_cts {I: BoundedInterval} {f:ℝ → ℝ} (hbound: BddOn f I
have h'const : PiecewiseConstantOn h' I := by
rw [of_join hjoin2 _]; and_intros
. rw [of_join hjoin1 _]; and_intros
. exact of_const (ConstantOn.of_const h'const_left)
. exact (ConstantOn.of_const h'const_left).piecewiseConstantOn
apply hhconst.congr'
intro x hx; simp [h', hx, mem_iff]
exact of_const (ConstantOn.of_const h'const_right)
exact (ConstantOn.of_const h'const_right).piecewiseConstantOn
have h'maj : MajorizesOn h' f I := by
intro x hx; by_cases hxI': x ∈ I' <;> simp [h', hxI']
. solve_by_elim
Expand Down Expand Up @@ -204,10 +204,10 @@ theorem integ_of_bdd_cts {I: BoundedInterval} {f:ℝ → ℝ} (hbound: BddOn f I
and_intros
. rw [of_join hjoin1 _]
and_intros
. exact of_const (ConstantOn.of_const g'const_left)
. exact (ConstantOn.of_const g'const_left).piecewiseConstantOn
apply hgconst.congr'
intro x hx; simp [g', hx, mem_iff]
exact of_const (ConstantOn.of_const g'const_right)
exact (ConstantOn.of_const g'const_right).piecewiseConstantOn
have g'maj : MinorizesOn g' f I := by
intro x hx; by_cases hxI': x ∈ I' <;> simp [g', hxI']
. solve_by_elim
Expand Down
Loading
Loading