From 1d6e2a631f54b19c45fe0193b91c1952d327aa33 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 22 Jul 2024 01:17:47 +0200 Subject: [PATCH 01/16] Update ComplexInterpolation.lean --- BonnAnalysis/ComplexInterpolation.lean | 455 +++++++++++-------------- 1 file changed, 193 insertions(+), 262 deletions(-) diff --git a/BonnAnalysis/ComplexInterpolation.lean b/BonnAnalysis/ComplexInterpolation.lean index 32c74e4..93dcbeb 100644 --- a/BonnAnalysis/ComplexInterpolation.lean +++ b/BonnAnalysis/ComplexInterpolation.lean @@ -37,42 +37,35 @@ lemma Real.rpow_le_rpow_iff_left {M:ℝ} (hM: M>0) (a b : ℝ) : M^a ≤ M^b ↔ simp } -lemma Real.le_one_of_add_nonneg_eq_one {t s : ℝ} (hs : 0 ≤ s) (hts : t + s = 1) : t ≤ 1 := by{ +lemma Real.le_one_of_add_nonneg_eq_one {t s : ℝ} (hs : 0 ≤ s) (hts : t + s = 1) : t ≤ 1 := calc t = 1 - s := eq_sub_of_add_eq hts - _ ≤ 1 := by simp[hs] -} + _ ≤ 1 := sub_le_self 1 hs -lemma pow_bound₀ {M:ℝ} (hM: M > 0) {z: ℂ} (hz: z.re ∈ Icc 0 1) : Complex.abs (M^(z-1)) ≤ max 1 (1/M) := by{ - rw[Complex.abs_cpow_eq_rpow_re_of_pos hM (z-1)] - simp - simp at hz +lemma pow_bound₀ {M:ℝ} (hM: M > 0) {z: ℂ} (hz: z.re ∈ Icc 0 1) : Complex.abs (M^(z-1)) ≤ max 1 (1/M) := by + rw [Complex.abs_cpow_eq_rpow_re_of_pos hM (z - 1), sub_re, one_re, one_div, le_max_iff] + simp only [mem_Icc] at hz by_cases h: M ≥ 1 · left have : 1 = M^0 := rfl nth_rewrite 2 [this] have := (Real.rpow_le_rpow_iff_left hM (z.re-1) 0).mpr - simp at this + simp only [tsub_le_iff_right, zero_add, sub_nonneg, Real.rpow_zero] at this apply this left - constructor - · exact h - · simp[hz.2] + exact ⟨h, by simp [hz.2]⟩ · right have : M^(-1:ℝ) = M⁻¹ := by apply Real.rpow_neg_one - rw[← this] + rw [← this] have := (Real.rpow_le_rpow_iff_left hM (z.re-1) (-1:ℝ)).mpr simp at this apply this right - constructor - · simp at h; exact le_of_lt h - · exact hz.1 -} + exact ⟨by simp only [ge_iff_le, not_le] at h; exact le_of_lt h, hz.1⟩ -- very similar proof to the previous one lemma pow_bound₁ {M:ℝ} (hM: M > 0) {z: ℂ} (hz: z.re ∈ Icc 0 1) : Complex.abs (M^(-z)) ≤ max 1 (1/M) := by{ - rw[Complex.abs_cpow_eq_rpow_re_of_pos hM (-z)] + rw [Complex.abs_cpow_eq_rpow_re_of_pos hM (-z)] simp simp at hz by_cases h: M ≥ 1 @@ -83,75 +76,58 @@ lemma pow_bound₁ {M:ℝ} (hM: M > 0) {z: ℂ} (hz: z.re ∈ Icc 0 1) : Complex simp at this apply this left - constructor - · exact h - · simp[hz.1] + exact ⟨h, by simp [hz.1]⟩ · right have : M^(-1:ℝ) = M⁻¹ := by apply Real.rpow_neg_one - rw[← this] + rw [← this] have := (Real.rpow_le_rpow_iff_left hM (-z.re) (-1:ℝ)).mpr simp at this apply this right - constructor - · simp at h; exact le_of_lt h - · exact hz.2 + exact ⟨by simp at h; exact le_of_lt h, hz.2⟩ } -lemma abs_fun_nonempty (f: ℂ → ℂ) : ((fun z ↦ Complex.abs (f z))'' { z | z.re ∈ Icc 0 1}).Nonempty := by{ - simp - use 0 - simp -} +lemma abs_fun_nonempty (f : ℂ → ℂ) : + ((fun z ↦ Complex.abs (f z))'' { z | z.re ∈ Icc 0 1 }).Nonempty := by + simp only [mem_Icc, image_nonempty] + exact ⟨0, by simp⟩ lemma abs_fun_bounded {f:ℂ → ℂ} (h2f : IsBounded (f '' { z | z.re ∈ Icc 0 1})) : BddAbove ((fun z ↦ Complex.abs (f z))'' { z | z.re ∈ Icc 0 1}) := by{ - simp[BddAbove, upperBounds] + simp [BddAbove, upperBounds] obtain ⟨R, hR⟩:= (isBounded_iff_forall_norm_le).mp h2f use R simp intro r z hz₁ hz₂ habs - rw[← habs] - exact hR (f z) (by use z; simp[hz₁, hz₂]) + rw [← habs] + exact hR (f z) (by use z; simp [hz₁, hz₂]) } /- Some technical lemmas to apply the maximum modulus principle -/ -lemma strip_prod : { z:ℂ | z.re ∈ Ioo 0 1} = (Ioo 0 1 : Set ℝ) ×ℂ univ := by{ +lemma strip_prod : { z:ℂ | z.re ∈ Ioo 0 1} = (Ioo 0 1 : Set ℝ) ×ℂ univ := by ext z - simp[Complex.mem_reProdIm] -} + simp [Complex.mem_reProdIm] -lemma clstrip_prod : {z: ℂ | z.re ∈ Icc 0 1} = (Icc 0 1 : Set ℝ) ×ℂ univ := by{ +lemma clstrip_prod : {z: ℂ | z.re ∈ Icc 0 1} = (Icc 0 1 : Set ℝ) ×ℂ univ := by ext z - simp[Complex.mem_reProdIm] -} + simp [Complex.mem_reProdIm] - -lemma isPreconnected_strip : IsPreconnected { z : ℂ | z.re ∈ Ioo 0 1} := by{ - have : { z : ℂ | z.re ∈ Ioo 0 1} = ⇑equivRealProdCLM.toHomeomorph ⁻¹' ((Ioo 0 1 : Set ℝ) ×ˢ (univ: Set ℝ)) := by{ +lemma isPreconnected_strip : IsPreconnected { z : ℂ | z.re ∈ Ioo 0 1} := by + have : { z : ℂ | z.re ∈ Ioo 0 1} = ⇑equivRealProdCLM.toHomeomorph ⁻¹' ((Ioo 0 1 : Set ℝ) ×ˢ (univ: Set ℝ)) := by ext z simp - } - rw[this, Homeomorph.isPreconnected_preimage Complex.equivRealProdCLM.toHomeomorph] + rw [this, Homeomorph.isPreconnected_preimage Complex.equivRealProdCLM.toHomeomorph] exact IsPreconnected.prod isPreconnected_Ioo isPreconnected_univ -} -lemma isOpen_strip : IsOpen { z : ℂ | z.re ∈ Ioo 0 1} := by{ - rw[strip_prod] - exact IsOpen.reProdIm isOpen_Ioo isOpen_univ -} -lemma isClosed_clstrip : IsClosed { z : ℂ | z.re ∈ Icc 0 1} := by{ - rw[clstrip_prod] - exact IsClosed.reProdIm isClosed_Icc isClosed_univ -} +lemma isOpen_strip : IsOpen { z : ℂ | z.re ∈ Ioo 0 1} := + strip_prod ▸ IsOpen.reProdIm isOpen_Ioo isOpen_univ +lemma isClosed_clstrip : IsClosed { z : ℂ | z.re ∈ Icc 0 1} := + clstrip_prod ▸ IsClosed.reProdIm isClosed_Icc isClosed_univ -lemma closure_strip : closure { z:ℂ | z.re ∈ Ioo 0 1} = { z: ℂ | z.re ∈ Icc 0 1} := by{ - rw[strip_prod, clstrip_prod] - rw [Complex.closure_reProdIm, closure_univ, closure_Ioo] - norm_num -} - +lemma closure_strip : closure { z:ℂ | z.re ∈ Ioo 0 1} = { z: ℂ | z.re ∈ Icc 0 1} := by + rw [strip_prod, clstrip_prod, Complex.closure_reProdIm, closure_univ, closure_Ioo] + exact zero_ne_one' ℝ /-- Hadamard's three lines lemma/theorem on the unit strip with bounds M₀=M₁=1 and vanishing at infinity condition. -/ theorem DiffContOnCl.norm_le_pow_mul_pow''' {f : ℂ → ℂ} @@ -167,92 +143,76 @@ theorem DiffContOnCl.norm_le_pow_mul_pow''' {f : ℂ → ℂ} obtain ⟨z, hz⟩ := Classical.axiom_of_choice hu3 have hzu : (norm ∘ f) ∘ z = u := by{ funext n - specialize hz n - rw[← hz.2] + rw [← (hz n).2] rfl } - have hrange₁ : range z ⊆ {w | (0 ≤ w.re ∧ w.re ≤ 1)} := by{ - simp[range] - intro n - specialize hz n - exact hz.1 - } - - have hrangeclos : closure (range z) ⊆ {w | (0 ≤ w.re ∧ w.re ≤ 1)} := by{ - apply (IsClosed.closure_subset_iff isClosed_clstrip).mpr - simp - exact hrange₁ - } + have hrange₁ : range z ⊆ {w | (0 ≤ w.re ∧ w.re ≤ 1)} := by + simp only [range, setOf_subset_setOf, forall_exists_index, forall_apply_eq_imp_iff] + exact fun n ↦ (hz n).1 + have hrangeclos : closure (range z) ⊆ {w | (0 ≤ w.re ∧ w.re ≤ 1)} := + (IsClosed.closure_subset_iff isClosed_clstrip).mpr hrange₁ have hbz : IsBounded (range z) := by{ have : Disjoint (Bornology.cobounded ℂ ⊓ Filter.principal ({ z: ℂ | z.re ∈ Icc 0 1})) (Filter.map z atTop) := by{ apply Tendsto.disjoint (f:= norm ∘ f) (lb₁ := nhds 0) (lb₂ := (nhds (sSup ((fun z ↦ Complex.abs (f z)) '' {z | z.re ∈ Icc 0 1})))) · have : norm ∘ f = (fun z ↦ Complex.abs (f z) ) := by rfl - rw[this] + rw [this] nth_rewrite 2 [← @norm_zero ℂ _] - apply Filter.Tendsto.norm - exact hlim - · simp + exact Filter.Tendsto.norm hlim + · simp only [mem_Icc, disjoint_nhds_nhds, ne_eq] apply ne_of_lt obtain ⟨w, hw1, hw2⟩ := h calc 0 < Complex.abs (f w) := hw2 - _ ≤ sSup ((fun z ↦ Complex.abs (f z)) '' {z | 0 ≤ z.re ∧ z.re ≤ 1}) := le_csSup (abs_fun_bounded h2f) (by simp; use w; simp at hw1; simp[hw1]) - · simp - rw[hzu] - simp at hu2 + _ ≤ sSup ((fun z ↦ Complex.abs (f z)) '' {z | 0 ≤ z.re ∧ z.re ≤ 1}) := le_csSup (abs_fun_bounded h2f) (by simp; use w; simp at hw1; simp [hw1]) + · simp only [mem_Icc, tendsto_map'_iff, hzu] exact hu2 } - rw[Filter.disjoint_iff] at this + rw [Filter.disjoint_iff] at this obtain ⟨A,hA, B, hB, hAB⟩ := this - rw[Filter.mem_map] at hB + rw [Filter.mem_map] at hB simp at hB obtain ⟨N, hN⟩ := hB have hB' : IsBounded (B ∩ {w : ℂ | w.re ∈ Icc 0 1}) := by{ obtain ⟨A₁, hA₁, A₂, hA₂, hAint⟩ := Filter.mem_inf_iff.mp hA - rw[hAint] at hAB - have : A₁ ∩ A₂ = (A₁ᶜ ∪ A₂ᶜ)ᶜ := by simp - rw[this, Set.disjoint_compl_left_iff_subset] at hAB - have hint' : A₂ᶜ ∩ {w | w.re ∈ Icc 0 1} = ∅ := by{ - rw[mem_principal] at hA₂ - rw[← Set.diff_eq_compl_inter, Set.diff_eq_empty] + rw [hAint] at hAB + have : A₁ ∩ A₂ = (A₁ᶜ ∪ A₂ᶜ)ᶜ := inter_eq_compl_compl_union_compl A₁ A₂ + rw [this, Set.disjoint_compl_left_iff_subset] at hAB + have hint' : A₂ᶜ ∩ {w | w.re ∈ Icc 0 1} = ∅ := by + rw [← Set.diff_eq_compl_inter, Set.diff_eq_empty] exact hA₂ - } have : B ∩ {w | w.re ∈ Icc 0 1} ⊆ A₁ᶜ := by{ calc B ∩ {w | w.re ∈ Icc 0 1} ⊆ (A₁ᶜ ∪ A₂ᶜ) ∩ {w | w.re ∈ Icc 0 1} := inter_subset_inter hAB (by simp) _ = (A₁ᶜ ∩ {w | w.re ∈ Icc 0 1}) ∪ (A₂ᶜ ∩ {w | w.re ∈ Icc 0 1}) := union_inter_distrib_right A₁ᶜ A₂ᶜ {w | w.re ∈ Icc 0 1} - _ = A₁ᶜ ∩ {w | w.re ∈ Icc 0 1} := by rw[hint']; simp + _ = A₁ᶜ ∩ {w | w.re ∈ Icc 0 1} := by rw [hint']; simp _ ⊆ A₁ᶜ := inter_subset_left } - apply Bornology.IsBounded.subset ?_ this - exact IsCobounded.compl hA₁ + exact Bornology.IsBounded.subset (IsCobounded.compl hA₁) this } - rw[isBounded_iff_forall_norm_le] at hB' + rw [isBounded_iff_forall_norm_le] at hB' obtain ⟨M, hM⟩ := hB' - have hbd : IsBounded (range (fun (i: Fin N) ↦ ‖ z i‖ )) := by{ - apply Set.Finite.isBounded - apply Set.finite_range - } + have hbd : IsBounded (range (fun (i: Fin N) ↦ ‖ z i‖ )) := + Set.Finite.isBounded (Set.finite_range _) obtain ⟨M', hM'⟩ := isBounded_iff_forall_norm_le.mp hbd simp at hM' - rw[isBounded_iff_forall_norm_le] + rw [isBounded_iff_forall_norm_le] use max M M' intro x hx simp at hx obtain ⟨n, hn⟩ := hx - rw[← hn] + rw [← hn] by_cases hc: N ≤ n · specialize hN n hc - specialize hM (z n) (by simp[hN]; specialize hz n; simp[hz]) + specialize hM (z n) (by simp [hN]; specialize hz n; simp [hz]) calc _ ≤ _ := hM _ ≤ _ := le_max_left M M' @@ -267,20 +227,20 @@ theorem DiffContOnCl.norm_le_pow_mul_pow''' {f : ℂ → ℂ} obtain ⟨z',hz', φ, hφ₁, hφ₂⟩ := tendsto_subseq_of_bounded (x:=z) hbz (by simp) have hu': Tendsto u atTop (nhds (Complex.abs (f z'))) := by { - rw[tendsto_iff_tendsto_subseq_of_monotone hu1 (StrictMono.tendsto_atTop hφ₁)] - rw[← hzu] + rw [tendsto_iff_tendsto_subseq_of_monotone hu1 (StrictMono.tendsto_atTop hφ₁)] + rw [← hzu] apply Tendsto.comp (y:= nhdsWithin z' {w:ℂ | w.re ∈ Icc 0 1}) · have hz'strip : z' ∈ {w | 0 ≤ w.re ∧ w.re ≤ 1} := by { - rw[subset_def] at hrangeclos + rw [subset_def] at hrangeclos exact hrangeclos z' hz' } have := ContinuousOn.restrict (DiffContOnCl.continuousOn hf) - rw[closure_strip] at this + rw [closure_strip] at this simp at this simp apply Tendsto.comp (y:= nhds (f z')) · apply Continuous.tendsto continuous_norm - · rw[tendsto_nhdsWithin_iff_subtype hz'strip] + · rw [tendsto_nhdsWithin_iff_subtype hz'strip] apply Continuous.tendsto exact this · apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within @@ -295,46 +255,40 @@ theorem DiffContOnCl.norm_le_pow_mul_pow''' {f : ℂ → ℂ} have hsup : Complex.abs (f z') = sSup ((fun z ↦ Complex.abs (f z)) '' {z | z.re ∈ Icc 0 1}) := tendsto_nhds_unique hu' hu2 have hmax : IsMaxOn (norm ∘ f) { w:ℂ | w.re ∈ Icc 0 1} z' := by{ - simp[IsMaxOn, IsMaxFilter] - intro w hw₁ hw₂ - rw[hsup] - apply le_csSup_of_le (abs_fun_bounded h2f) (b:= Complex.abs (f w)) ?_ (by simp) - simp - use w + simp only [IsMaxOn, IsMaxFilter, Function.comp_apply, norm_eq_abs, mem_Icc, + eventually_principal, mem_setOf_eq, and_imp] + exact fun w hw₁ hw₂ ↦ hsup ▸ le_csSup_of_le (abs_fun_bounded h2f) (b:= Complex.abs (f w)) + (by simp; use w) (by simp) } have hmax' : IsMaxOn (norm ∘ f) { w:ℂ | w.re ∈ Ioo 0 1} z' := by{ apply IsMaxOn.on_subset hmax - simp; intro z hz₁ hz₂ - constructor - · exact le_of_lt hz₁ - · exact le_of_lt hz₂ + simp only [mem_Ioo, mem_Icc, setOf_subset_setOf, and_imp] + exact fun z hz₁ hz₂ ↦ ⟨le_of_lt hz₁, le_of_lt hz₂⟩ } by_cases h : z' ∈ { w : ℂ | w.re ∈ Ioo 0 1} · have := Complex.norm_eqOn_closure_of_isPreconnected_of_isMaxOn (isPreconnected_strip) (isOpen_strip) hf h hmax' - simp[EqOn] at this + simp [EqOn] at this have h0 : Complex.abs (f 0) = Complex.abs (f z') := by{ apply this have hcl := closure_strip simp at hcl - rw[hcl] + rw [hcl] simp } have hpt : Complex.abs (f (t + I*y)) = Complex.abs (f z') := by { apply this have hcl := closure_strip simp at hcl - rw[hcl] - simp - constructor - · exact ht - · exact Real.le_one_of_add_nonneg_eq_one hs hts + rw [hcl, mem_setOf_eq, add_re, ofReal_re, mul_re, I_re, zero_mul, I_im, ofReal_im, + mul_zero, sub_self, add_zero] + exact ⟨ht, Real.le_one_of_add_nonneg_eq_one hs hts⟩ } simp - rw[hpt, ← h0] + rw [hpt, ← h0] specialize h₀f 0 simp at h₀f exact h₀f @@ -352,7 +306,7 @@ theorem DiffContOnCl.norm_le_pow_mul_pow''' {f : ℂ → ℂ} specialize h (lt_of_le_of_ne this.1 (Ne.symm hc) ) exact eq_of_le_of_le this.2 h } - simp[IsMaxOn, IsMaxFilter] at hmax + simp [IsMaxOn, IsMaxFilter] at hmax specialize hmax (t+I*y) simp at hmax specialize hmax ht (Real.le_one_of_add_nonneg_eq_one hs hts) @@ -360,26 +314,25 @@ theorem DiffContOnCl.norm_le_pow_mul_pow''' {f : ℂ → ℂ} · specialize h₀f (z'.im) have : z' = I * z'.im := by { nth_rewrite 1 [← Complex.re_add_im z'] - simp[hz'₁, mul_comm] + simp [hz'₁, mul_comm] } - rw[this] at hmax + rw [this] at hmax calc _ ≤ _ := hmax _ ≤ _ := h₀f · specialize h₁f (z'.im) have : z' = 1 + I * z'.im := by { nth_rewrite 1 [← Complex.re_add_im z'] - simp[hz'₂, mul_comm] + simp [hz'₂, mul_comm] } - rw[this] at hmax + rw [this] at hmax calc _ ≤ _ := hmax _ ≤ _ := h₁f · simp at h specialize h (t + I * y) simp at h - specialize h ht (Real.le_one_of_add_nonneg_eq_one hs hts) - rw[h] + rw [h ht (Real.le_one_of_add_nonneg_eq_one hs hts)] simp } @@ -391,7 +344,7 @@ def bump (ε: ℝ) : ℂ → ℂ := fun z ↦ exp (ε * (z^2 -1)) lemma bump_diffcontoncl (ε : ℝ) : DiffContOnCl ℂ (bump ε) { z | z.re ∈ Ioo 0 1} := by{ refine Differentiable.diffContOnCl ?h have h' : bump ε = exp ∘ (fun z ↦ ε * (z^2 -1) ) := rfl - rw[h'] + rw [h'] apply Differentiable.comp · exact differentiable_exp · simp @@ -407,7 +360,7 @@ lemma perturb_diffcontoncl {f: ℂ → ℂ} (hf : DiffContOnCl ℂ f { z | z.re lemma perturb_bound (f: ℂ → ℂ) (ε : ℝ) (z : ℂ) : Complex.abs (perturb f ε z) ≤ Complex.abs (f z) * Real.exp (ε * ((z.re)^2 - 1 - (z.im)^2)) := by{ - simp[perturb, bump] + simp [perturb, bump] gcongr nth_rewrite 1 [Complex.abs_exp, ← Complex.re_add_im z, add_sq'] simp @@ -415,7 +368,7 @@ lemma perturb_bound (f: ℂ → ℂ) (ε : ℝ) (z : ℂ) : Complex.abs (perturb simp left norm_cast - rw[mul_pow, Complex.I_sq] + rw [mul_pow, Complex.I_sq] simp norm_cast ring @@ -423,8 +376,8 @@ lemma perturb_bound (f: ℂ → ℂ) (ε : ℝ) (z : ℂ) : Complex.abs (perturb lemma bound_factor_le_one {ε : ℝ} (hε: ε > 0) {z : ℂ} (hz: z.re ∈ Icc 0 1) : Real.exp (ε * ((z.re)^2 - 1 - (z.im)^2)) ≤ 1 := by{ simp at hz - rw[Real.exp_le_one_iff] - rw[mul_nonpos_iff] + rw [Real.exp_le_one_iff] + rw [mul_nonpos_iff] left constructor · exact le_of_lt hε @@ -432,7 +385,7 @@ lemma bound_factor_le_one {ε : ℝ} (hε: ε > 0) {z : ℂ} (hz: z.re ∈ Icc 0 z.re ^ 2 - 1 - z.im ^ 2 ≤ z.re ^ 2 - 1 := by{ simp; exact sq_nonneg z.im} _ ≤ 0 := by { simp - rw[abs_le] + rw [abs_le] constructor · calc -1 ≤ 0 := by norm_num @@ -443,19 +396,19 @@ lemma bound_factor_le_one {ε : ℝ} (hε: ε > 0) {z : ℂ} (hz: z.re ∈ Icc 0 lemma perturb_isbounded {f: ℂ → ℂ} (h2f : IsBounded (f '' { z | z.re ∈ Icc 0 1})) {ε : ℝ} (hε: ε>0) : IsBounded ((perturb f ε) '' { z | z.re ∈ Icc 0 1}) := by{ - rw[isBounded_iff_forall_norm_le] + rw [isBounded_iff_forall_norm_le] obtain ⟨R, hR⟩:= (isBounded_iff_forall_norm_le).mp h2f use R intro x hx simp at hx obtain ⟨z, hz₁, hz₂⟩ := hx - rw[← hz₂] + rw [← hz₂] specialize hR (f z) (by use z; simp; exact hz₁) simp calc _ ≤ _ := perturb_bound f ε z _ ≤ R := by { - rw[← mul_one R] + rw [← mul_one R] gcongr · calc _ ≤ _ := AbsoluteValue.nonneg Complex.abs (f z) @@ -470,8 +423,8 @@ lemma perturb_bound_left {f: ℂ → ℂ} (h₀f : ∀ y : ℝ, ‖f (I * y)‖ have hb := perturb_bound f ε (I*y) simp at hb have : (ε * (-1 - y ^ 2)).exp ≤ 1 := by{ - rw[Real.exp_le_one_iff] - rw[mul_nonpos_iff] + rw [Real.exp_le_one_iff] + rw [mul_nonpos_iff] left constructor · exact le_of_lt hε @@ -492,9 +445,9 @@ lemma perturb_bound_right {f: ℂ → ℂ} (h₁f : ∀ y : ℝ, ‖f (1 + I * y simp at hb have : (-(ε * y ^ 2)).exp ≤ 1 := by{ - rw[Real.exp_le_one_iff] + rw [Real.exp_le_one_iff] simp - rw[mul_nonneg_iff] + rw [mul_nonneg_iff] left constructor · exact le_of_lt hε @@ -507,22 +460,22 @@ lemma perturb_bound_right {f: ℂ → ℂ} (h₁f : ∀ y : ℝ, ‖f (1 + I * y } lemma perturb_vanish_infty {f:ℂ → ℂ} (h2f : IsBounded (f '' { z | z.re ∈ Icc 0 1})) {ε : ℝ} (hε: ε > 0) : Tendsto (perturb f ε) (Bornology.cobounded ℂ ⊓ Filter.principal ({ z: ℂ | z.re ∈ Icc 0 1})) (nhds 0) := by{ - simp[Tendsto] + simp [Tendsto] intro A hA - rw[mem_map, Filter.mem_inf_iff] + rw [mem_map, Filter.mem_inf_iff] simp use { z | z.re ∈ Icc 0 1}ᶜ ∪ (perturb f ε)⁻¹' A constructor - · rw[← Bornology.isCobounded_def, ← Bornology.isBounded_compl_iff] + · rw [← Bornology.isCobounded_def, ← Bornology.isBounded_compl_iff] simp - rw[isBounded_iff_forall_norm_le] + rw [isBounded_iff_forall_norm_le] simp obtain ⟨r, hr₁, hr₂⟩ := Metric.eventually_nhds_iff_ball.mp (eventually_closedBall_subset hA) - specialize hr₂ (r/2) (by simp; rw[abs_of_pos hr₁]; simp; exact hr₁) + specialize hr₂ (r/2) (by simp; rw [abs_of_pos hr₁]; simp; exact hr₁) obtain ⟨M, hM⟩ := isBounded_iff_forall_norm_le.mp h2f have hM' : 0 < M ∨ 0 = M := by{ --this could indeed be zero if the function f is constantly zero - rw[← le_iff_lt_or_eq] + rw [← le_iff_lt_or_eq] specialize hM (f 0) (by use 0; simp) calc 0 ≤ Complex.abs (f 0) := AbsoluteValue.nonneg Complex.abs (f 0) @@ -533,58 +486,58 @@ lemma perturb_vanish_infty {f:ℂ → ℂ} (h2f : IsBounded (f '' { z | z.re ∈ intro z hz₁ hz₂ hz₃ have hball := Set.not_mem_subset hr₂ hz₃ simp at hball - rw[Complex.abs_eq_sqrt_sq_add_sq] + rw [Complex.abs_eq_sqrt_sq_add_sq] apply Real.sqrt_le_sqrt gcongr - · rw[sq_le_one_iff hz₁]; exact hz₂ - · rw[← mul_le_mul_left hε, ← mul_comm_div, div_self (ne_of_gt hε)] + · rw [sq_le_one_iff hz₁]; exact hz₂ + · rw [← mul_le_mul_left hε, ← mul_comm_div, div_self (ne_of_gt hε)] simp have : r/2 < M * Real.exp (ε * ((z.re)^2 - 1 - (z.im)^2)) := by{ calc _ < _ := hball _ ≤ _ := perturb_bound f ε z - _ ≤ _ := by {gcongr; specialize hM (f z) (by use z; simp[hz₁, hz₂]); exact hM} + _ ≤ _ := by {gcongr; specialize hM (f z) (by use z; simp [hz₁, hz₂]); exact hM} } - have hr₁' : r/2 > 0 := by simp[hr₁] + have hr₁' : r/2 > 0 := by simp [hr₁] have hrhs : 0 < M * Real.exp (ε * (z.re ^ 2 - 1 - z.im ^ 2)) := by{ apply Real.mul_pos hM'₁ apply Real.exp_pos } - rw[← Real.log_lt_log_iff hr₁' hrhs, Real.log_mul (ne_of_gt hM'₁) (by apply Real.exp_ne_zero), Real.log_exp] at this + rw [← Real.log_lt_log_iff hr₁' hrhs, Real.log_mul (ne_of_gt hM'₁) (by apply Real.exp_ne_zero), Real.log_exp] at this apply le_of_lt - rw[← add_lt_add_iff_right (Real.log (r/2))] + rw [← add_lt_add_iff_right (Real.log (r/2))] simp have haux : ε * (z.re ^ 2 - 1 - z.im ^ 2) = ε * (z.re^2 - 1) - ε * z.im^2 := by ring - rw[haux, ← add_sub_assoc, ← add_lt_add_iff_right (ε * z.im ^ 2)] at this + rw [haux, ← add_sub_assoc, ← add_lt_add_iff_right (ε * z.im ^ 2)] at this simp at this - rw[add_comm] + rw [add_comm] have hre : ε * (z.re ^ 2 - 1) ≤ 0 := by{ - rw[mul_nonpos_iff] + rw [mul_nonpos_iff] left constructor · exact le_of_lt hε - · simp; rw[_root_.abs_of_nonneg hz₁]; exact hz₂ + · simp; rw [_root_.abs_of_nonneg hz₁]; exact hz₂ } calc _ < _ := this - _ ≤ Real.log M := by simp[hre] + _ ≤ Real.log M := by simp [hre] · use 0 --Any number works here intro z hz₁ hz₂ hz₃ -- hz₃ cannot happen, so we get a contradiction have hA' := mem_of_mem_nhds hA have : perturb f ε z = 0 := by{ - simp[perturb]; left - rw[← AbsoluteValue.eq_zero Complex.abs] + simp [perturb]; left + rw [← AbsoluteValue.eq_zero Complex.abs] apply eq_of_le_of_le - · specialize hM (f z) (by use z; simp[hz₁, hz₂]) - rw[← hM'₂] at hM + · specialize hM (f z) (by use z; simp [hz₁, hz₂]) + rw [← hM'₂] at hM exact hM · exact AbsoluteValue.nonneg Complex.abs (f z) } - rw[this] at hz₃ + rw [this] at hz₃ contradiction · use { z | z.re ∈ Icc 0 1} ∪ (perturb f ε)⁻¹' A constructor @@ -592,7 +545,7 @@ lemma perturb_vanish_infty {f:ℂ → ℂ} (h2f : IsBounded (f '' { z | z.re ∈ · ext z constructor · intro h - simp[h] + simp [h] · intro h simp at h obtain ⟨h1, h2⟩ := h @@ -601,60 +554,42 @@ lemma perturb_vanish_infty {f:ℂ → ℂ} (h2f : IsBounded (f '' { z | z.re ∈ · specialize hc1 hd1.1 have : (1: ℝ) < (1:ℝ ) := by { calc - 1 < z.re := by simp[hc1] - _ ≤ 1 := by simp[hd1.2] + 1 < z.re := by simp [hc1] + _ ≤ 1 := by simp [hd1.2] } norm_num at this - · simp[hd2] - · simp[hc2] + · simp [hd2] + · simp [hc2] } - lemma perturb_bound_strip {f : ℂ → ℂ} {ε : ℝ} (hε: ε > 0) (hf : DiffContOnCl ℂ f { z | z.re ∈ Ioo 0 1}) (h2f : IsBounded (f '' { z | z.re ∈ Icc 0 1})) (h₀f : ∀ y : ℝ, ‖f (I * y)‖ ≤ 1) (h₁f : ∀ y : ℝ, ‖f (1 + I * y)‖ ≤ 1) - {y t s : ℝ} (ht : 0 ≤ t) (hs : 0 ≤ s) (hts : t + s = 1) : ‖perturb f ε (t + I*y)‖ ≤ 1 := by { - apply DiffContOnCl.norm_le_pow_mul_pow''' ?_ ?_ ?_ ?_ ht hs hts ?_ - · exact perturb_diffcontoncl hf ε - · exact perturb_isbounded h2f hε - · exact perturb_bound_left h₀f hε - · exact perturb_bound_right h₁f hε - · exact perturb_vanish_infty h2f hε - } - + {y t s : ℝ} (ht : 0 ≤ t) (hs : 0 ≤ s) (hts : t + s = 1) : ‖perturb f ε (t + I*y)‖ ≤ 1 := + DiffContOnCl.norm_le_pow_mul_pow''' (perturb_diffcontoncl hf ε) (perturb_isbounded h2f hε) + (perturb_bound_left h₀f hε) (perturb_bound_right h₁f hε) ht hs hts (perturb_vanish_infty h2f hε) -lemma perturb_pointwise_converge {f : ℂ → ℂ} (z: ℂ) : Tendsto (fun ε ↦ perturb f ε z) (nhds 0) (nhds (f z)) := by{ - simp[perturb] +lemma perturb_pointwise_converge {f : ℂ → ℂ} (z: ℂ) : Tendsto (fun ε ↦ perturb f ε z) (nhds 0) (nhds (f z)) := by + simp [perturb] have : (fun ε ↦ f z * bump ε z) = fun ε ↦ (((fun _ ↦ f z) ε) * ((fun t ↦ bump t z) ε)) := rfl - rw[this] + rw [this] have : f z = f z * 1 := by simp nth_rewrite 2 [this] - apply Filter.Tendsto.mul - · exact tendsto_const_nhds - · have : bump 0 z = 1 := by simp[bump] - rw[← this] - apply Continuous.tendsto (x:=0) - simp[bump] - have : (fun (x:ℝ) ↦ cexp (↑x * (z ^ 2 - 1))) = cexp ∘ (fun x ↦ x * (z^2 - 1)) ∘ (fun (x:ℝ) ↦ (x:ℂ)) := rfl - rw[this] - apply Continuous.comp - · exact continuous_exp - · apply Continuous.comp - · exact continuous_mul_right (z ^ 2 - 1) - · exact Complex.continuous_ofReal -} - - -lemma perturb_pointwise_norm_converge (f : ℂ → ℂ) (z: ℂ) : Tendsto (fun ε ↦ Complex.abs (perturb f ε z)) (nhdsWithin 0 (Ioi 0)) (nhds (Complex.abs (f z))) := by{ + refine Filter.Tendsto.mul tendsto_const_nhds ?_ + have : bump 0 z = 1 := by simp [bump] + rw [← this] + apply Continuous.tendsto (x := 0) + simp [bump] + have : (fun (x:ℝ) ↦ cexp (↑x * (z ^ 2 - 1))) = cexp ∘ (fun x ↦ x * (z^2 - 1)) ∘ (fun (x:ℝ) ↦ (x:ℂ)) := rfl + rw [this] + exact continuous_exp.comp ((continuous_mul_right (z ^ 2 - 1)).comp Complex.continuous_ofReal) + +lemma perturb_pointwise_norm_converge (f : ℂ → ℂ) (z: ℂ) : + Tendsto (fun ε ↦ Complex.abs (perturb f ε z)) (nhdsWithin 0 (Ioi 0)) (nhds (Complex.abs (f z))) := by have : (fun ε ↦ Complex.abs (perturb f ε z)) = Complex.abs ∘ (fun ε ↦ perturb f ε z) := rfl - rw[this] - apply Tendsto.comp (y:= nhds (f z)) - · apply Continuous.tendsto - exact Complex.continuous_abs - · apply Filter.Tendsto.mono_left (perturb_pointwise_converge z) - apply nhdsWithin_le_nhds -} + exact this ▸ Tendsto.comp (y:= nhds (f z)) (Continuous.tendsto Complex.continuous_abs _) + (Filter.Tendsto.mono_left (perturb_pointwise_converge z) nhdsWithin_le_nhds) /-- Hadamard's three lines lemma/theorem on the unit strip with bounds M₀=M₁=1. -/ theorem DiffContOnCl.norm_le_pow_mul_pow'' {f : ℂ → ℂ} @@ -665,23 +600,19 @@ theorem DiffContOnCl.norm_le_pow_mul_pow'' {f : ℂ → ℂ} ‖f (t + I * y)‖ ≤ 1 := by{ have := perturb_pointwise_norm_converge f (t+I*y) apply @le_of_tendsto _ _ _ _ _ (fun ε ↦ Complex.abs (perturb f ε (t + I * y))) _ _ _ _ this - rw[eventually_nhdsWithin_iff] + rw [eventually_nhdsWithin_iff] filter_upwards with ε hε - simp at hε + simp only [mem_Ioi] at hε exact perturb_bound_strip hε hf h2f h₀f h₁f ht hs hts } -lemma DiffContOnCl.const_cpow {a: ℂ} (ha: a ≠ 0) {s: Set ℂ} {f: ℂ → ℂ} (hf: DiffContOnCl ℂ f s) : DiffContOnCl ℂ (fun (z:ℂ) ↦ a^ (f z)) s := by{ - apply DiffContOnCl.mk - · apply DifferentiableOn.const_cpow - · exact hf.differentiableOn - · left; exact ha - · apply ContinuousOn.const_cpow - · exact hf.continuousOn - · left; exact ha -} +lemma DiffContOnCl.const_cpow {a: ℂ} (ha: a ≠ 0) {s: Set ℂ} {f: ℂ → ℂ} (hf: DiffContOnCl ℂ f s) : + DiffContOnCl ℂ (fun (z:ℂ) ↦ a^ (f z)) s := + DiffContOnCl.mk (DifferentiableOn.const_cpow hf.differentiableOn (Or.inl ha)) + (ContinuousOn.const_cpow hf.continuousOn (Or.inl ha)) -lemma DiffContOnCl.id [NormedSpace ℂ E] {s: Set E} : DiffContOnCl ℂ (fun x : E ↦ x) s := DiffContOnCl.mk differentiableOn_id continuousOn_id +lemma DiffContOnCl.id [NormedSpace ℂ E] {s: Set E} : DiffContOnCl ℂ (fun x : E ↦ x) s := + DiffContOnCl.mk differentiableOn_id continuousOn_id -- needed for fun_prop lemma DiffContOnCl.neg' [NormedSpace ℂ E] [NormedSpace ℂ E₂] {f : E → E₂} {s: Set E} @@ -705,23 +636,23 @@ theorem DiffContOnCl.norm_le_pow_mul_pow₀₁ {f : ℂ → ℂ} let h : ℂ → ℂ := fun z ↦ p₁ z • p₂ z have hsmul : g = fun z ↦ h z • f z := rfl have hg: DiffContOnCl ℂ g { z | z.re ∈ Ioo 0 1} := by { - rw[hsmul] + rw [hsmul] fun_prop (discharger := norm_cast; positivity) } have h2g: IsBounded (g '' { z | z.re ∈ Icc 0 1}) := by { obtain ⟨R, hR⟩ := isBounded_iff_forall_norm_le.mp h2f - rw[isBounded_iff_forall_norm_le] + rw [isBounded_iff_forall_norm_le] let A := max 1 (1/M₀) let B := max 1 (1/M₁) use A*B*R intro w hw simp at hw obtain ⟨z, hz₁, hz₂, hz₃⟩ := hw - simp[g] + simp [g] gcongr · apply pow_bound₀ hM₀ (by simp; exact hz₁) · apply pow_bound₁ hM₁ (by simp; exact hz₁) - · exact hR (f z) (by use z; simp[hz₁]) + · exact hR (f z) (by use z; simp [hz₁]) } have h₀g : ∀ y : ℝ, ‖g (I * y)‖ ≤ 1 := by { @@ -739,9 +670,9 @@ theorem DiffContOnCl.norm_le_pow_mul_pow₀₁ {f : ℂ → ℂ} simp } - rw[h₁, h₂] + rw [h₁, h₂] simp - rw[← inv_mul_cancel (ne_of_gt hM₀)] + rw [← inv_mul_cancel (ne_of_gt hM₀)] gcongr exact h₀f y } @@ -763,16 +694,16 @@ theorem DiffContOnCl.norm_le_pow_mul_pow₀₁ {f : ℂ → ℂ} simp } - rw[h₁, h₂] + rw [h₁, h₂] simp - rw[← inv_mul_cancel (ne_of_gt hM₁)] + rw [← inv_mul_cancel (ne_of_gt hM₁)] gcongr exact h₁f y } have hgoal := DiffContOnCl.norm_le_pow_mul_pow'' hg h2g h₀g h₁g ht hs hts (y:=y) - simp[g] at hgoal - simp[hgoal] + simp [g] at hgoal + simp [hgoal] --This is also essentially the same thing I did before to prove the bounds, so yet more duplicate code have h₁: Complex.abs (↑M₀ ^ (↑t + I * ↑y - 1)) = M₀ ^ (t-1) := by{ @@ -785,17 +716,17 @@ theorem DiffContOnCl.norm_le_pow_mul_pow₀₁ {f : ℂ → ℂ} simp } - rw[h₁, h₂] at hgoal + rw [h₁, h₂] at hgoal have hM₁': M₁^(-t)>0 := Real.rpow_pos_of_pos hM₁ (-t) have hM₀': M₀^(t-1)>0 := Real.rpow_pos_of_pos hM₀ (t-1) - rw[← mul_le_mul_left hM₁',← mul_le_mul_left hM₀'] + rw [← mul_le_mul_left hM₁',← mul_le_mul_left hM₀'] nth_rewrite 2 [mul_comm (M₁^(-t)), ← mul_assoc] - rw[mul_assoc, mul_assoc, ← Real.rpow_add hM₁ t (-t)] - simp[eq_sub_of_add_eq (add_comm t s ▸ hts)] - rw[ ← Real.rpow_add hM₀ (t-1) (1-t)] + rw [mul_assoc, mul_assoc, ← Real.rpow_add hM₁ t (-t)] + simp [eq_sub_of_add_eq (add_comm t s ▸ hts)] + rw [ ← Real.rpow_add hM₀ (t-1) (1-t)] simp - rw[← mul_assoc] + rw [← mul_assoc] exact hgoal } @@ -809,19 +740,19 @@ theorem DiffContOnCl.norm_le_pow_mul_pow {a b : ℝ} {f : ℂ → ℂ} (hab: a Date: Mon, 22 Jul 2024 01:17:49 +0200 Subject: [PATCH 02/16] Update Dual.lean --- BonnAnalysis/Dual.lean | 92 +++++++++++++++++++++--------------------- 1 file changed, 46 insertions(+), 46 deletions(-) diff --git a/BonnAnalysis/Dual.lean b/BonnAnalysis/Dual.lean index 8633c7b..91f1bd9 100644 --- a/BonnAnalysis/Dual.lean +++ b/BonnAnalysis/Dual.lean @@ -346,18 +346,18 @@ theorem snorm'_mul_const {p : ℝ} (hp : p > 0) (f : α → ℝ) (c : ℝ) : conv => pattern (_ * _) ^ _ - rw[ENNReal.mul_rpow_of_ne_top] + rw [ENNReal.mul_rpow_of_ne_top] rfl apply coe_ne_top apply coe_ne_top - rw[lintegral_mul_const'] + rw [lintegral_mul_const'] case neg.hr => simp_all by_cases hf : ∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ = ∞ - . rw[hf]; simp_all + . rw [hf]; simp_all - rw[ENNReal.mul_rpow_of_ne_top hf] + rw [ENNReal.mul_rpow_of_ne_top hf] case neg.hy => simp_all; congr @@ -410,14 +410,14 @@ theorem nnnorm_of_sign (x) : ‖Real.sign x‖₊ = if x = 0 then 0 else 1 := by theorem Real.self_mul_sign (x : ℝ) : x * x.sign = |x| := by by_cases hx₁ : x = 0 - . rw[hx₁, Real.sign_zero, mul_zero, abs_zero] + . rw [hx₁, Real.sign_zero, mul_zero, abs_zero] . by_cases hx₂ : x > 0 - . rw[Real.sign_of_pos hx₂, mul_one, abs_of_pos hx₂] + . rw [Real.sign_of_pos hx₂, mul_one, abs_of_pos hx₂] . have hx₃ : x < 0 := by apply lt_of_le_of_ne linarith exact hx₁ - rw[Real.sign_of_neg hx₃, mul_neg_one, abs_of_neg hx₃] + rw [Real.sign_of_neg hx₃, mul_neg_one, abs_of_neg hx₃] theorem rpow_of_nnnorm_of_sign (x y : ℝ) (hypos : y > 0) : (‖Real.sign x‖₊ : ℝ≥0∞) ^ y = if x = 0 then 0 else 1 := by aesop @@ -429,13 +429,13 @@ theorem rpow'_eq_rpow (x : ℝ≥0) (y : ℝ) : rpow' y x = x^y := rfl theorem ennreal_rpow_of_nnreal (x : ℝ≥0) (y : ℝ) : (ENNReal.rpow x y).toNNReal = NNReal.rpow x y := by simp only [ENNReal.rpow_eq_pow, NNReal.rpow_eq_pow] - rw[←ENNReal.toNNReal_rpow] + rw [←ENNReal.toNNReal_rpow] simp only [ENNReal.toNNReal_coe] theorem ennreal_rpow_of_nnreal' (x : ℝ≥0) (y : ℝ) (hynneg : y ≥ 0) : ENNReal.rpow x y = ofNNReal (NNReal.rpow x y) := by apply (ENNReal.toNNReal_eq_toNNReal_iff' _ _).mp <;> simp - . rw[←ENNReal.toNNReal_rpow, ENNReal.toNNReal_coe] + . rw [←ENNReal.toNNReal_rpow, ENNReal.toNNReal_coe] . intro _; assumption theorem measurable_rpow'_const (c : ℝ) : Measurable (rpow' c) := @@ -472,7 +472,7 @@ theorem mul_of_ae_eq {f f' g g' : α → ℝ≥0∞} (hf : f =ᵐ[μ] f') (hg : theorem mul_of_ae_eq_one (f g: α → ℝ≥0∞) (hf : f =ᵐ[μ] 1) : f * g =ᵐ[μ] g := by conv => rhs - rw[←one_mul g] + rw [←one_mul g] apply mul_of_ae_eq hf trivial @@ -522,9 +522,9 @@ theorem lint_conj_q_lt_top'_mul_self (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} simp congr . congr - rw[mul_comm, Real.toNNReal_mul, ENNReal.toNNReal_eq_toNNreal_of_toReal] - . rw[ENNReal.coe_rpow_of_nonneg] - . rw[ENNReal.toNNReal_coe] + rw [mul_comm, Real.toNNReal_mul, ENNReal.toNNReal_eq_toNNreal_of_toReal] + . rw [ENNReal.coe_rpow_of_nonneg] + . rw [ENNReal.toNNReal_coe] rfl . apply q_sub_one_nneg' (p := p) hqᵢ . apply toReal_nonneg @@ -538,11 +538,11 @@ theorem int_conj_q_lt_top'_mul_self (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} unfold ENNReal.rpow' conv => pattern _ * _ - rw[mul_assoc, mul_comm, mul_assoc] + rw [mul_assoc, mul_comm, mul_assoc] congr rfl - rw[Real.self_mul_sign] - rw[←nnnorm_toReal_eq_abs] + rw [Real.self_mul_sign] + rw [←nnnorm_toReal_eq_abs] rfl sorry @@ -587,10 +587,10 @@ theorem snorm'_of_conj_q_lt_top' (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) : snorm' (conj_q_lt_top' g) p.toReal μ = (snorm' g q.toReal μ) ^ (q.toReal - 1) := by unfold snorm' - rw[←ENNReal.rpow_mul, ←q_div_p_add_one'' (q := q) (p := p) hqᵢ] - rw[←mul_div_right_comm (a := 1) (c := q.toReal)] - rw[one_mul, div_div, div_mul_cancel_right₀ (q_ne_zero' (p := p) hqᵢ) (a := p.toReal)] - rw[inv_eq_one_div] + rw [←ENNReal.rpow_mul, ←q_div_p_add_one'' (q := q) (p := p) hqᵢ] + rw [←mul_div_right_comm (a := 1) (c := q.toReal)] + rw [one_mul, div_div, div_mul_cancel_right₀ (q_ne_zero' (p := p) hqᵢ) (a := p.toReal)] + rw [inv_eq_one_div] congr 1 unfold conj_q_lt_top' @@ -599,19 +599,19 @@ theorem snorm'_of_conj_q_lt_top' (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) conv => lhs pattern _ ^ _ - rw[nnnorm_mul, ENNReal.coe_mul, (ENNReal.mul_rpow_of_nonneg _ _ p_ge_zero')] + rw [nnnorm_mul, ENNReal.coe_mul, (ENNReal.mul_rpow_of_nonneg _ _ p_ge_zero')] congr rfl - rw[ENNReal.coe_rpow_of_nonneg _ p_ge_zero'] + rw [ENNReal.coe_rpow_of_nonneg _ p_ge_zero'] congr - rw[←Real.toNNReal_eq_nnnorm_of_nonneg toReal_nonneg] - rw[toNNReal_eq_toNNreal_of_toReal, ENNReal.toNNReal_rpow] + rw [←Real.toNNReal_eq_nnnorm_of_nonneg toReal_nonneg] + rw [toNNReal_eq_toNNreal_of_toReal, ENNReal.toNNReal_rpow] congr dsimp [ENNReal.rpow] - rw[←ENNReal.rpow_mul] + rw [←ENNReal.rpow_mul] congr rfl - rw[sub_mul (c := p.toReal), one_mul, mul_comm, ←p_add_q' hqᵢ] + rw [sub_mul (c := p.toReal), one_mul, mul_comm, ←p_add_q' hqᵢ] simp rfl @@ -620,10 +620,10 @@ theorem snorm'_of_conj_q_lt_top' (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) pattern _*_ congr - . rw[rpow_of_nnnorm_of_sign _ _ p_gt_zero'] + . rw [rpow_of_nnnorm_of_sign _ _ p_gt_zero'] rfl - . rw[ENNReal.coe_toNNReal] + . rw [ENNReal.coe_toNNReal] rfl apply ENNReal.rpow_of_to_ENNReal_of_NNReal_ne_top _ _ q_ge_zero' @@ -634,7 +634,7 @@ theorem snorm'_of_conj_q_lt_top' (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) conv => lhs pattern _ ^ _ - rw[ENNReal.zero_rpow_of_pos (q_gt_zero' hqᵢ)] + rw [ENNReal.zero_rpow_of_pos (q_gt_zero' hqᵢ)] rfl simp @@ -652,7 +652,7 @@ theorem snorm_of_conj_q_lt_top' (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) theorem Memℒp_conj_q_lt_top' (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) : Memℒp (conj_q_lt_top' g) p μ := by constructor . measurability - . rw[snorm_of_conj_q_lt_top' hqᵢ g] + . rw [snorm_of_conj_q_lt_top' hqᵢ g] exact ENNReal.rpow_lt_top_of_nonneg (q_sub_one_nneg' (p := p) hqᵢ) (snorm_ne_top g) def conj_q_lt_top (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) : Lp ℝ p μ := @@ -668,7 +668,7 @@ theorem snorm_of_conj_q_lt_top (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) @[simp] theorem norm_of_conj_q_lt_top (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) : ‖conj_q_lt_top (p := p) hqᵢ g‖ = ‖g‖ ^ (q.toReal - 1) := by - rw[norm_def, norm_def, ENNReal.toReal_rpow] + rw [norm_def, norm_def, ENNReal.toReal_rpow] congr exact snorm_of_conj_q_lt_top (p := p) hqᵢ g @@ -701,7 +701,7 @@ theorem snorm'_normalized_conj_q_lt_top' {g : Lp ℝ q μ} (hqᵢ : q ≠ ∞) ( unfold normalized_conj_q_lt_top' unfold rpow' - rw[snorm'_mul_const p_gt_zero', + rw [snorm'_mul_const p_gt_zero', snorm'_of_conj_q_lt_top' hqᵢ, NNReal.rpow_eq_pow, coe_rpow, @@ -716,30 +716,30 @@ theorem snorm'_normalized_conj_q_lt_top' {g : Lp ℝ q μ} (hqᵢ : q ≠ ∞) ( generalize hy : q.toReal - 1 = y have y_pos : y > 0 := by - calc _ = q.toReal - 1 := by rw[hy] + calc _ = q.toReal - 1 := by rw [hy] _ > 1 - 1 := by gcongr; apply q_gt_one' (p := p) hqᵢ _ = 0 := by ring have y_nneg : y ≥ 0 := by linarith[y_pos] - have x_ne_top : x ≠ ∞ := by rw[←hx]; exact snorm_ne_top g + have x_ne_top : x ≠ ∞ := by rw [←hx]; exact snorm_ne_top g have x_ne_zero : x ≠ 0 := by - calc _ = snorm g q μ := by rw[hx] - _ = (snorm g q μ).toNNReal := by symm; apply ENNReal.coe_toNNReal; rw[hx]; exact x_ne_top - _ = ‖g‖₊ := by rw[nnnorm_def] + calc _ = snorm g q μ := by rw [hx] + _ = (snorm g q μ).toNNReal := by symm; apply ENNReal.coe_toNNReal; rw [hx]; exact x_ne_top + _ = ‖g‖₊ := by rw [nnnorm_def] _ ≠ 0 := by apply ENNReal.coe_ne_zero.mpr; exact hg have x_rpow_y_ne_top : x^y ≠ ∞ := ENNReal.rpow_ne_top_of_nonneg y_nneg x_ne_top - rw[←ENNReal.coe_toNNReal (a := x ^ y) x_rpow_y_ne_top, + rw [←ENNReal.coe_toNNReal (a := x ^ y) x_rpow_y_ne_top, ENNReal.toReal_rpow, ENNReal.nnnorm_of_toReal_eq_toNNReal] norm_cast - rw[←ENNReal.toNNReal_mul, + rw [←ENNReal.toNNReal_mul, ←ENNReal.one_toNNReal] congr - rw[←ENNReal.rpow_add] + rw [←ENNReal.rpow_add] . simp . exact x_ne_zero . exact x_ne_top @@ -747,7 +747,7 @@ theorem snorm'_normalized_conj_q_lt_top' {g : Lp ℝ q μ} (hqᵢ : q ≠ ∞) ( @[simp] theorem snorm_normalized_conj_q_lt_top' (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} (hg : ‖g‖₊ ≠ 0) : snorm (normalized_conj_q_lt_top' g) p μ = 1 := by - rw[snorm_eq_snorm'] + rw [snorm_eq_snorm'] exact snorm'_normalized_conj_q_lt_top' hqᵢ hg exact p_ne_zero (q := q) exact p_ne_top (p := p) @@ -756,7 +756,7 @@ theorem Memℒp_normalized_conj_q_lt_top' (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} : Memℒp (normalized_conj_q_lt_top' g) p μ := by constructor . exact normalized_conj_q_lt_top'_aestrongly_measurable g - . rw[snorm_normalized_conj_q_lt_top' hqᵢ hg] + . rw [snorm_normalized_conj_q_lt_top' hqᵢ hg] trivial def normalized_conj_q_lt_top (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} (hg : ‖g‖₊ ≠ 0) : Lp ℝ p μ := @@ -773,7 +773,7 @@ theorem snorm_normalized_conj_q_lt_top (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} (hg @[simp] theorem norm_of_normalized_conj_q_lt_top (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} (hg : ‖g‖₊ ≠ 0) : ‖normalized_conj_q_lt_top (p := p) hqᵢ hg‖ = 1 := by - rw[norm_def, ←ENNReal.one_toReal] + rw [norm_def, ←ENNReal.one_toReal] congr exact snorm_normalized_conj_q_lt_top (p := p) hqᵢ hg @@ -807,7 +807,7 @@ theorem snorm_eq_sup_q_gt_top (g : Lp ℝ q μ) (hqᵢ : q ≠ ∞) : swap; sorry constructor . simp only [Set.mem_setOf_eq] - rw[norm_of_normalized_conj_q_lt_top] + rw [norm_of_normalized_conj_q_lt_top] . dsimp only exact int_normalized_conj_q_lt_top_mul_self (p := p) hqᵢ (?_ : ‖g‖₊ ≠ 0) @@ -819,9 +819,9 @@ theorem snorm_eq_sup_q_gt_top (g : Lp ℝ q μ) (hqᵢ : q ≠ ∞) : calc _ ≤ ∫ x, ‖f x * g x‖ ∂μ := by apply norm_integral_le_integral_norm _ = ∫ x, ‖(mul ℝ ℝ) (f x) (g x)‖ ∂μ := by simp only [norm_mul, norm_eq_abs, mul_apply'] _ ≤ ‖(mul ℝ ℝ)‖ * ‖f‖ * ‖g‖ := by apply integral_mul_le; exact hpq.out - _ = ‖f‖ * ‖g‖ := by rw[opNorm_mul, one_mul] + _ = ‖f‖ * ‖g‖ := by rw [opNorm_mul, one_mul] _ ≤ 1 * ‖g‖ := by gcongr - _ = ‖g‖ := by rw[one_mul] + _ = ‖g‖ := by rw [one_mul] variable (p q μ) in theorem snorm_eq_sup_abs (hμ : SigmaFinite μ) (g : Lp ℝ q μ): From 5b7734b66925d9ed981b9a0c0df89bddf9f578e1 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 22 Jul 2024 01:17:50 +0200 Subject: [PATCH 03/16] Update Plancherel.lean --- BonnAnalysis/Plancherel.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/BonnAnalysis/Plancherel.lean b/BonnAnalysis/Plancherel.lean index 6484f46..67bb2b1 100644 --- a/BonnAnalysis/Plancherel.lean +++ b/BonnAnalysis/Plancherel.lean @@ -47,7 +47,7 @@ instance : NormedAddCommGroup (V →₁₂[volume] E) := simp [snorm_congr_ae (AEEqFun.coeFn_add f g), snorm_add_le ((Lp.mem_Lp_iff_memℒp.1 hf).1) ((Lp.mem_Lp_iff_memℒp.1 hg).1)]) ((Lp.mem_Lp_iff_snorm_lt_top.1 hf).ne) ((Lp.mem_Lp_iff_snorm_lt_top.1 hg).ne) - neg' := by simp[snorm_congr_ae (AEEqFun.coeFn_neg _)] + neg' := by simp [ snorm_congr_ae (AEEqFun.coeFn_neg _)] eq_zero_of_map_eq_zero' := by intro ⟨f, _, hf⟩ h simp [ENNReal.toReal_eq_zero_iff] at h From 287ebb96d66ce4db074e91a494c13e2b7972a452 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 22 Jul 2024 02:53:07 +0200 Subject: [PATCH 04/16] Update ComplexInterpolation.lean --- BonnAnalysis/ComplexInterpolation.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/BonnAnalysis/ComplexInterpolation.lean b/BonnAnalysis/ComplexInterpolation.lean index 93dcbeb..75eb6e5 100644 --- a/BonnAnalysis/ComplexInterpolation.lean +++ b/BonnAnalysis/ComplexInterpolation.lean @@ -1133,7 +1133,8 @@ lemma lintegral_mul_le_segment_exponent {p₀ p₁ p : ℝ≥0∞} {s t : ℝ≥ one_mul, le_refl] rcases eq_or_ne p ⊤ with hpt | hpt' - . simp [hpt, add_eq_zero, hs0', ht0'] at hp + . simp only [hpt, inv_top, add_eq_zero, ENNReal.div_eq_zero_iff, ENNReal.coe_eq_zero, hs0', + false_or, ht0'] at hp exact False.elim <| ne_top_of_lt hp₀₁ hp.1 . calc snorm f p μ = (∫⁻ (a : α), ↑‖f a‖₊ ^ p.toReal ∂μ) ^ p.toReal⁻¹ := by simp [snorm, hp0', hpt', snorm'] From 7f1fdde0fb36c9581d5aa1f6dd2f424589ee6136 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 22 Jul 2024 02:53:10 +0200 Subject: [PATCH 05/16] Update Dual.lean --- BonnAnalysis/Dual.lean | 77 ++++++++++++++++++------------------------ 1 file changed, 32 insertions(+), 45 deletions(-) diff --git a/BonnAnalysis/Dual.lean b/BonnAnalysis/Dual.lean index 91f1bd9..2b2c6a8 100644 --- a/BonnAnalysis/Dual.lean +++ b/BonnAnalysis/Dual.lean @@ -110,8 +110,7 @@ lemma mul_eq_add (hpq : p.IsConjExponent q) : p * q = p + q := by . simp [hpq.right_ne_zero] induction q . simp [hpq.left_ne_zero] - norm_cast - exact hpq.toNNReal coe_ne_top coe_ne_top |>.mul_eq_add + exact_mod_cast hpq.toNNReal coe_ne_top coe_ne_top |>.mul_eq_add lemma induction (P : (p q : ℝ≥0∞) → (p.IsConjExponent q) → Prop) @@ -158,7 +157,8 @@ lemma _root_.ENNReal.lintegral_mul_le_one_top (μ : Measure α) {f g : α → lemma _root_.ENNReal.lintegral_norm_mul_le_one_top (μ : Measure α) {f : α → E₁} {g : α → E₂} (hf : AEMeasurable f μ) : ∫⁻ a, ‖f a‖₊ * ‖g a‖₊ ∂μ ≤ snorm f 1 μ * snorm g ⊤ μ := by - simp [snorm, snorm', snormEssSup] + simp only [snorm, one_ne_zero, ↓reduceIte, one_ne_top, snorm', one_toReal, rpow_one, ne_eq, + not_false_eq_true, div_self, top_ne_zero, snormEssSup] exact lintegral_mul_le_one_top _ hf.ennnorm theorem lintegral_mul_le (hpq : p.IsConjExponent q) (μ : Measure α) {f : α → E₁} {g : α → E₂} @@ -213,7 +213,7 @@ def rpow' (y : ℝ) (x : ℝ≥0∞) : ℝ≥0∞ := ENNReal.rpow x y theorem rpow'_eq_rpow (x : ℝ≥0∞) (y : ℝ) : rpow' y x = x^y := rfl theorem measurable_rpow'_const (c : ℝ) : Measurable (rpow' c) := by - apply Measurable.pow (f := fun x => x) (g := fun _ => c) <;> measurability + apply Measurable.pow (f := fun x => x) (g := fun _ => c) <;> fun_prop end ENNReal @@ -274,22 +274,15 @@ lemma q_ge_zero' : q.toReal ≥ 0 := p_ge_zero' lemma q_gt_one : q > 1 := (left_ne_top_iff hpq.out).mp p_ne_top -lemma q_gt_one' (hqᵢ : q ≠ ∞) : q.toReal > 1 := by - rw [←ENNReal.one_toReal] - apply (ENNReal.toReal_lt_toReal _ _).mpr - . show q > 1 - apply q_gt_one (q := q) (p := p) - . exact Ne.symm top_ne_one - . exact hqᵢ +lemma q_gt_one' (hqᵢ : q ≠ ∞) : q.toReal > 1 := + ENNReal.one_toReal ▸ (ENNReal.toReal_lt_toReal (Ne.symm top_ne_one) hqᵢ).mpr + (q_gt_one (q := q) (p := p)) lemma q_ge_one : q ≥ 1 := by apply le_of_lt; exact q_gt_one (p := p) -lemma q_ge_one' (hqᵢ : q ≠ ∞) : q.toReal ≥ 1 := by - rw [← ENNReal.one_toReal] - apply (ENNReal.toReal_le_toReal _ _).mpr - . exact q_ge_one (q := q) (p := p) - . exact Ne.symm top_ne_one - . exact hqᵢ +lemma q_ge_one' (hqᵢ : q ≠ ∞) : q.toReal ≥ 1 := + ENNReal.one_toReal ▸ (ENNReal.toReal_le_toReal (Ne.symm top_ne_one) hqᵢ).mpr + (q_ge_one (q := q) (p := p)) lemma q_sub_one_pos' (hqᵢ : q ≠ ∞) : q.toReal - 1 > 0 := sub_pos.mpr (q_gt_one' (q := q) (p := p) hqᵢ) @@ -308,13 +301,11 @@ lemma q_div_p_ne_top (hqᵢ : q ≠ ∞) : q / p ≠ ∞ := by by_contra! have := (@ENNReal.div_eq_top q p).mp this contrapose! this - constructor - . intro _; exact (p_ne_zero (q := q)) - . intro _; contradiction + exact ⟨fun _ ↦ p_ne_zero (q := q), fun _ ↦ by contradiction⟩ lemma q_div_p_add_one : q / p + 1 = q := by - calc _ = q / p + p / p := by rw [ENNReal.div_self (p_ne_zero (q := q)) p_ne_top]; - _ = (q + p) / p := by rw [← ENNReal.add_div] + calc _ = q / p + p / p := by rw [ENNReal.div_self (p_ne_zero (q := q)) p_ne_top] + _ = (q + p) / p := ENNReal.div_add_div_same _ = (p + q) / p := by rw [add_comm] _ = (p * q) / p := by rw [p_add_q] _ = (p * q) / (p * 1) := by rw [mul_one] @@ -484,9 +475,8 @@ theorem integral_mul_le (hpq : p.IsConjExponent q) (μ : Measure α) {f : Lp E : ∫ a, ‖L (f a) (g a)‖ ∂μ ≤ ‖L‖ * ‖f‖ * ‖g‖ := by have : AEStronglyMeasurable (fun x => L (f x) (g x)) μ := - by apply L.aestronglyMeasurable_comp₂ - apply (Lp.memℒp f).aestronglyMeasurable - apply (Lp.memℒp g).aestronglyMeasurable + L.aestronglyMeasurable_comp₂ (Lp.memℒp f).aestronglyMeasurable (Lp.memℒp g).aestronglyMeasurable + rw [integral_norm_eq_lintegral_nnnorm this] have : (‖L‖₊ * (snorm f p μ) * (snorm g q μ)).toReal = ‖L‖ * ‖f‖ * ‖g‖ := by @@ -495,9 +485,9 @@ theorem integral_mul_le (hpq : p.IsConjExponent q) (μ : Measure α) {f : Lp E rw [←this] have : ∫⁻ (a : α), ↑‖(L (f a)) (g a)‖₊ ∂μ ≤ ↑‖L‖₊ * snorm (f) p μ * snorm (g) q μ := by - apply lintegral_mul_le L hpq μ - . exact aestronglyMeasurable_iff_aemeasurable.mp (Lp.memℒp f).aestronglyMeasurable - . exact aestronglyMeasurable_iff_aemeasurable.mp (Lp.memℒp g).aestronglyMeasurable + apply lintegral_mul_le L hpq μ (aestronglyMeasurable_iff_aemeasurable.mp + (Lp.memℒp f).aestronglyMeasurable) (aestronglyMeasurable_iff_aemeasurable.mp + (Lp.memℒp g).aestronglyMeasurable) gcongr apply mul_ne_top; apply mul_ne_top @@ -699,9 +689,7 @@ theorem normalized_conj_q_lt_top'_aestrongly_measurable (g : Lp ℝ q μ) theorem snorm'_normalized_conj_q_lt_top' {g : Lp ℝ q μ} (hqᵢ : q ≠ ∞) (hg : ‖g‖₊ ≠ 0) : snorm' (normalized_conj_q_lt_top' g) p.toReal μ = 1 := by unfold normalized_conj_q_lt_top' - unfold rpow' - - rw [snorm'_mul_const p_gt_zero', + rw [rpow', snorm'_mul_const p_gt_zero', snorm'_of_conj_q_lt_top' hqᵢ, NNReal.rpow_eq_pow, coe_rpow, @@ -722,13 +710,13 @@ theorem snorm'_normalized_conj_q_lt_top' {g : Lp ℝ q μ} (hqᵢ : q ≠ ∞) ( have y_nneg : y ≥ 0 := by linarith[y_pos] - have x_ne_top : x ≠ ∞ := by rw [←hx]; exact snorm_ne_top g + have x_ne_top : x ≠ ∞ := hx ▸ snorm_ne_top g have x_ne_zero : x ≠ 0 := by calc _ = snorm g q μ := by rw [hx] _ = (snorm g q μ).toNNReal := by symm; apply ENNReal.coe_toNNReal; rw [hx]; exact x_ne_top _ = ‖g‖₊ := by rw [nnnorm_def] - _ ≠ 0 := by apply ENNReal.coe_ne_zero.mpr; exact hg + _ ≠ 0 := ENNReal.coe_ne_zero.mpr hg have x_rpow_y_ne_top : x^y ≠ ∞ := ENNReal.rpow_ne_top_of_nonneg y_nneg x_ne_top @@ -748,9 +736,9 @@ theorem snorm'_normalized_conj_q_lt_top' {g : Lp ℝ q μ} (hqᵢ : q ≠ ∞) ( theorem snorm_normalized_conj_q_lt_top' (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} (hg : ‖g‖₊ ≠ 0) : snorm (normalized_conj_q_lt_top' g) p μ = 1 := by rw [snorm_eq_snorm'] - exact snorm'_normalized_conj_q_lt_top' hqᵢ hg - exact p_ne_zero (q := q) - exact p_ne_top (p := p) + · exact snorm'_normalized_conj_q_lt_top' hqᵢ hg + · exact p_ne_zero (q := q) + · exact p_ne_top (p := p) theorem Memℒp_normalized_conj_q_lt_top' (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} (hg : ‖g‖₊ ≠ 0) : Memℒp (normalized_conj_q_lt_top' g) p μ := by @@ -766,9 +754,9 @@ def normalized_conj_q_lt_top (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} (hg : ‖g‖ theorem snorm_normalized_conj_q_lt_top (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} (hg : ‖g‖₊ ≠ 0) : snorm (normalized_conj_q_lt_top (p := p) hqᵢ hg) p μ = 1 := by apply _root_.trans - show _ = snorm (normalized_conj_q_lt_top' g) p μ; swap - · exact snorm_normalized_conj_q_lt_top' hqᵢ hg + show _ = snorm (normalized_conj_q_lt_top' g) p μ; · exact snorm_congr_ae (coeFn_toLp _) + · exact snorm_normalized_conj_q_lt_top' hqᵢ hg @[simp] theorem norm_of_normalized_conj_q_lt_top (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} (hg : ‖g‖₊ ≠ 0) @@ -797,9 +785,9 @@ theorem snorm_eq_sup_q_gt_top (g : Lp ℝ q μ) (hqᵢ : q ≠ ∞) : rcases hx with ⟨f, hf, rfl⟩ dsimp at hf dsimp only - calc _ ≤ ∫ x, ‖f x * g x‖ ∂μ := by apply norm_integral_le_integral_norm - _ = ∫ x, ‖(mul ℝ ℝ) (f x) (g x)‖ ∂μ := by simp - _ ≤ ‖(mul ℝ ℝ)‖ * ‖f‖ * ‖g‖ := by apply integral_mul_le; exact hpq.out + calc _ ≤ ∫ x, ‖f x * g x‖ ∂μ := norm_integral_le_integral_norm _ + _ = ∫ x, ‖(mul ℝ ℝ) (f x) (g x)‖ ∂μ := rfl + _ ≤ ‖(mul ℝ ℝ)‖ * ‖f‖ * ‖g‖ := integral_mul_le _ hpq.out _ _ = ‖f‖ * ‖g‖ := by simp _ ≤ 1 * ‖g‖ := by gcongr _ = ‖g‖ := by simp @@ -811,14 +799,13 @@ theorem snorm_eq_sup_q_gt_top (g : Lp ℝ q μ) (hqᵢ : q ≠ ∞) : . dsimp only exact int_normalized_conj_q_lt_top_mul_self (p := p) hqᵢ (?_ : ‖g‖₊ ≠ 0) - . apply Real.sSup_le; swap; apply norm_nonneg - intro x hx + . refine Real.sSup_le (fun x hx ↦ ?_) (norm_nonneg _) rcases hx with ⟨f, hf, rfl⟩ simp at hf; dsimp only - calc _ ≤ ∫ x, ‖f x * g x‖ ∂μ := by apply norm_integral_le_integral_norm + calc _ ≤ ∫ x, ‖f x * g x‖ ∂μ := norm_integral_le_integral_norm _ _ = ∫ x, ‖(mul ℝ ℝ) (f x) (g x)‖ ∂μ := by simp only [norm_mul, norm_eq_abs, mul_apply'] - _ ≤ ‖(mul ℝ ℝ)‖ * ‖f‖ * ‖g‖ := by apply integral_mul_le; exact hpq.out + _ ≤ ‖(mul ℝ ℝ)‖ * ‖f‖ * ‖g‖ := integral_mul_le _ hpq.out _ _ = ‖f‖ * ‖g‖ := by rw [opNorm_mul, one_mul] _ ≤ 1 * ‖g‖ := by gcongr _ = ‖g‖ := by rw [one_mul] From 14bc5fa042f01d6fbdf7b491f7affdd1d523fdff Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 22 Jul 2024 10:02:24 +0200 Subject: [PATCH 06/16] Update ComplexInterpolation.lean --- BonnAnalysis/ComplexInterpolation.lean | 32 ++++++++------------------ 1 file changed, 10 insertions(+), 22 deletions(-) diff --git a/BonnAnalysis/ComplexInterpolation.lean b/BonnAnalysis/ComplexInterpolation.lean index 75eb6e5..e713463 100644 --- a/BonnAnalysis/ComplexInterpolation.lean +++ b/BonnAnalysis/ComplexInterpolation.lean @@ -689,9 +689,9 @@ theorem DiffContOnCl.norm_le_pow_mul_pow₀₁ {f : ℂ → ℂ} have h₂ : Complex.abs (↑M₁ ^ (-(I * ↑y) + (- 1))) = M₁⁻¹ := by{ rw [Complex.abs_cpow_eq_rpow_re_of_pos hM₁] - simp - norm_cast - simp + simp only [add_re, neg_re, mul_re, I_re, ofReal_re, zero_mul, I_im, ofReal_im, mul_zero, + sub_self, neg_zero, one_re, zero_add] + exact Real.rpow_neg_one M₁ } rw [h₁, h₂] @@ -738,10 +738,7 @@ theorem DiffContOnCl.norm_le_pow_mul_pow {a b : ℝ} {f : ℂ → ℂ} (hab: a Date: Mon, 22 Jul 2024 10:21:29 +0200 Subject: [PATCH 07/16] Update ComplexInterpolation.lean --- BonnAnalysis/ComplexInterpolation.lean | 90 +++++++++----------------- 1 file changed, 32 insertions(+), 58 deletions(-) diff --git a/BonnAnalysis/ComplexInterpolation.lean b/BonnAnalysis/ComplexInterpolation.lean index e713463..05d63f8 100644 --- a/BonnAnalysis/ComplexInterpolation.lean +++ b/BonnAnalysis/ComplexInterpolation.lean @@ -52,16 +52,13 @@ lemma pow_bound₀ {M:ℝ} (hM: M > 0) {z: ℂ} (hz: z.re ∈ Icc 0 1) : Complex have := (Real.rpow_le_rpow_iff_left hM (z.re-1) 0).mpr simp only [tsub_le_iff_right, zero_add, sub_nonneg, Real.rpow_zero] at this apply this - left - exact ⟨h, by simp [hz.2]⟩ + exact Or.inl ⟨h, by simp [hz.2]⟩ · right have : M^(-1:ℝ) = M⁻¹ := by apply Real.rpow_neg_one rw [← this] have := (Real.rpow_le_rpow_iff_left hM (z.re-1) (-1:ℝ)).mpr simp at this - apply this - right - exact ⟨by simp only [ge_iff_le, not_le] at h; exact le_of_lt h, hz.1⟩ + exact this (Or.inr ⟨by simp only [ge_iff_le, not_le] at h; exact le_of_lt h, hz.1⟩) -- very similar proof to the previous one lemma pow_bound₁ {M:ℝ} (hM: M > 0) {z: ℂ} (hz: z.re ∈ Icc 0 1) : Complex.abs (M^(-z)) ≤ max 1 (1/M) := by{ @@ -75,16 +72,13 @@ lemma pow_bound₁ {M:ℝ} (hM: M > 0) {z: ℂ} (hz: z.re ∈ Icc 0 1) : Complex have := (Real.rpow_le_rpow_iff_left hM (-z.re) 0).mpr simp at this apply this - left - exact ⟨h, by simp [hz.1]⟩ + exact Or.inl ⟨h, by simp [hz.1]⟩ · right have : M^(-1:ℝ) = M⁻¹ := by apply Real.rpow_neg_one rw [← this] have := (Real.rpow_le_rpow_iff_left hM (-z.re) (-1:ℝ)).mpr simp at this - apply this - right - exact ⟨by simp at h; exact le_of_lt h, hz.2⟩ + exact this (Or.inr ⟨by simp at h; exact le_of_lt h, hz.2⟩) } lemma abs_fun_nonempty (f : ℂ → ℂ) : @@ -301,9 +295,9 @@ theorem DiffContOnCl.norm_le_pow_mul_pow''' {f : ℂ → ℂ} tauto } by_cases hc: z'.re = 0 - · left; assumption + · exact Or.inl ‹_› · right - specialize h (lt_of_le_of_ne this.1 (Ne.symm hc) ) + specialize h (lt_of_le_of_ne this.1 (Ne.symm hc)) exact eq_of_le_of_le this.2 h } simp [IsMaxOn, IsMaxFilter] at hmax @@ -341,23 +335,16 @@ theorem DiffContOnCl.norm_le_pow_mul_pow''' {f : ℂ → ℂ} def bump (ε: ℝ) : ℂ → ℂ := fun z ↦ exp (ε * (z^2 -1)) -lemma bump_diffcontoncl (ε : ℝ) : DiffContOnCl ℂ (bump ε) { z | z.re ∈ Ioo 0 1} := by{ - refine Differentiable.diffContOnCl ?h +lemma bump_diffcontoncl (ε : ℝ) : DiffContOnCl ℂ (bump ε) { z | z.re ∈ Ioo 0 1} := by + refine Differentiable.diffContOnCl ?_ have h' : bump ε = exp ∘ (fun z ↦ ε * (z^2 -1) ) := rfl - rw [h'] - apply Differentiable.comp - · exact differentiable_exp - · simp -} + exact (h') ▸ Differentiable.comp differentiable_exp (by simp) def perturb (f: ℂ → ℂ) (ε : ℝ) : ℂ → ℂ := fun z ↦ (f z) • (bump ε z) -lemma perturb_diffcontoncl {f: ℂ → ℂ} (hf : DiffContOnCl ℂ f { z | z.re ∈ Ioo 0 1}) (ε : ℝ) : DiffContOnCl ℂ (perturb f ε) { z | z.re ∈ Ioo 0 1} := by{ - apply DiffContOnCl.smul - · exact hf - · exact bump_diffcontoncl ε -} - +lemma perturb_diffcontoncl {f: ℂ → ℂ} (hf : DiffContOnCl ℂ f { z | z.re ∈ Ioo 0 1}) (ε : ℝ) : + DiffContOnCl ℂ (perturb f ε) { z | z.re ∈ Ioo 0 1} := + DiffContOnCl.smul hf (bump_diffcontoncl ε) lemma perturb_bound (f: ℂ → ℂ) (ε : ℝ) (z : ℂ) : Complex.abs (perturb f ε z) ≤ Complex.abs (f z) * Real.exp (ε * ((z.re)^2 - 1 - (z.im)^2)) := by{ simp [perturb, bump] @@ -374,26 +361,20 @@ lemma perturb_bound (f: ℂ → ℂ) (ε : ℝ) (z : ℂ) : Complex.abs (perturb ring } -lemma bound_factor_le_one {ε : ℝ} (hε: ε > 0) {z : ℂ} (hz: z.re ∈ Icc 0 1) : Real.exp (ε * ((z.re)^2 - 1 - (z.im)^2)) ≤ 1 := by{ +lemma bound_factor_le_one {ε : ℝ} (hε: ε > 0) {z : ℂ} (hz: z.re ∈ Icc 0 1) : Real.exp (ε * ((z.re)^2 - 1 - (z.im)^2)) ≤ 1 := by simp at hz - rw [Real.exp_le_one_iff] - rw [mul_nonpos_iff] + rw [Real.exp_le_one_iff, mul_nonpos_iff] left - constructor - · exact le_of_lt hε - · calc - z.re ^ 2 - 1 - z.im ^ 2 ≤ z.re ^ 2 - 1 := by{ simp; exact sq_nonneg z.im} - _ ≤ 0 := by { - simp - rw [abs_le] - constructor - · calc - -1 ≤ 0 := by norm_num - _ ≤ z.re := hz.1 - · exact hz.2 - } -} - + refine ⟨le_of_lt hε, ?_⟩ + calc + z.re ^ 2 - 1 - z.im ^ 2 ≤ z.re ^ 2 - 1 := by simp; exact sq_nonneg z.im + _ ≤ 0 := by + simp + rw [abs_le] + refine ⟨?_, hz.2⟩ + · calc + -1 ≤ 0 := by norm_num + _ ≤ z.re := hz.1 lemma perturb_isbounded {f: ℂ → ℂ} (h2f : IsBounded (f '' { z | z.re ∈ Icc 0 1})) {ε : ℝ} (hε: ε>0) : IsBounded ((perturb f ε) '' { z | z.re ∈ Icc 0 1}) := by{ rw [isBounded_iff_forall_norm_le] @@ -423,15 +404,13 @@ lemma perturb_bound_left {f: ℂ → ℂ} (h₀f : ∀ y : ℝ, ‖f (I * y)‖ have hb := perturb_bound f ε (I*y) simp at hb have : (ε * (-1 - y ^ 2)).exp ≤ 1 := by{ - rw [Real.exp_le_one_iff] - rw [mul_nonpos_iff] + rw [Real.exp_le_one_iff, mul_nonpos_iff] left - constructor - · exact le_of_lt hε - · simp - calc - -1 ≤ 0 := by norm_num - _ ≤ y^2 := sq_nonneg y + refine ⟨le_of_lt hε, ?_⟩ + simp + calc + -1 ≤ 0 := by norm_num + _ ≤ y^2 := sq_nonneg y } calc Complex.abs (perturb f ε (I * ↑y)) ≤ Complex.abs (f (I * ↑y)) * (ε * (-1 - y ^ 2)).exp := hb @@ -448,10 +427,7 @@ lemma perturb_bound_right {f: ℂ → ℂ} (h₁f : ∀ y : ℝ, ‖f (1 + I * y rw [Real.exp_le_one_iff] simp rw [mul_nonneg_iff] - left - constructor - · exact le_of_lt hε - · exact sq_nonneg y + exact Or.inl ⟨le_of_lt hε, sq_nonneg y⟩ } calc Complex.abs (perturb f ε (1 + I * ↑y)) ≤ Complex.abs (f (1 + I * ↑y)) * (-(ε * y ^ 2)).exp := hb @@ -515,9 +491,7 @@ lemma perturb_vanish_infty {f:ℂ → ℂ} (h2f : IsBounded (f '' { z | z.re ∈ have hre : ε * (z.re ^ 2 - 1) ≤ 0 := by{ rw [mul_nonpos_iff] left - constructor - · exact le_of_lt hε - · simp; rw [_root_.abs_of_nonneg hz₁]; exact hz₂ + exact ⟨le_of_lt hε, by simp; rw [_root_.abs_of_nonneg hz₁]; exact hz₂⟩ } calc From 592707dd2cf59730e72b442a49d8c8a3fbd199dd Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 22 Jul 2024 10:27:37 +0200 Subject: [PATCH 08/16] Update ComplexInterpolation.lean --- BonnAnalysis/ComplexInterpolation.lean | 30 +++++++++----------------- 1 file changed, 10 insertions(+), 20 deletions(-) diff --git a/BonnAnalysis/ComplexInterpolation.lean b/BonnAnalysis/ComplexInterpolation.lean index 05d63f8..f77ce05 100644 --- a/BonnAnalysis/ComplexInterpolation.lean +++ b/BonnAnalysis/ComplexInterpolation.lean @@ -364,8 +364,7 @@ lemma perturb_bound (f: ℂ → ℂ) (ε : ℝ) (z : ℂ) : Complex.abs (perturb lemma bound_factor_le_one {ε : ℝ} (hε: ε > 0) {z : ℂ} (hz: z.re ∈ Icc 0 1) : Real.exp (ε * ((z.re)^2 - 1 - (z.im)^2)) ≤ 1 := by simp at hz rw [Real.exp_le_one_iff, mul_nonpos_iff] - left - refine ⟨le_of_lt hε, ?_⟩ + refine Or.inl ⟨le_of_lt hε, ?_⟩ calc z.re ^ 2 - 1 - z.im ^ 2 ≤ z.re ^ 2 - 1 := by simp; exact sq_nonneg z.im _ ≤ 0 := by @@ -405,8 +404,7 @@ lemma perturb_bound_left {f: ℂ → ℂ} (h₀f : ∀ y : ℝ, ‖f (I * y)‖ simp at hb have : (ε * (-1 - y ^ 2)).exp ≤ 1 := by{ rw [Real.exp_le_one_iff, mul_nonpos_iff] - left - refine ⟨le_of_lt hε, ?_⟩ + refine Or.inl ⟨le_of_lt hε, ?_⟩ simp calc -1 ≤ 0 := by norm_num @@ -490,8 +488,7 @@ lemma perturb_vanish_infty {f:ℂ → ℂ} (h2f : IsBounded (f '' { z | z.re ∈ rw [add_comm] have hre : ε * (z.re ^ 2 - 1) ≤ 0 := by{ rw [mul_nonpos_iff] - left - exact ⟨le_of_lt hε, by simp; rw [_root_.abs_of_nonneg hz₁]; exact hz₂⟩ + exact Or.inl ⟨le_of_lt hε, by simp; rw [_root_.abs_of_nonneg hz₁]; exact hz₂⟩ } calc @@ -724,8 +721,7 @@ theorem DiffContOnCl.norm_le_pow_mul_pow {a b : ℝ} {f : ℂ → ℂ} (hab: a Date: Mon, 22 Jul 2024 10:37:32 +0200 Subject: [PATCH 09/16] Update Dual.lean --- BonnAnalysis/Dual.lean | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/BonnAnalysis/Dual.lean b/BonnAnalysis/Dual.lean index 2b2c6a8..6e1b2ff 100644 --- a/BonnAnalysis/Dual.lean +++ b/BonnAnalysis/Dual.lean @@ -143,17 +143,17 @@ Note that the hard case already exists as `ENNReal.lintegral_mul_le_Lp_mul_Lq`. lemma _root_.ContinuousLinearMap.le_opNNNorm₂ (L : E₁ →L[𝕜] E₂ →L[𝕜] E₃) (x : E₁) (y : E₂) : ‖L x y‖₊ ≤ ‖L‖₊ * ‖x‖₊ * ‖y‖₊ := L.le_opNorm₂ x y -lemma _root_.ENNReal.lintegral_mul_le_one_top (μ : Measure α) {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) : - ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ∂μ) * (essSup g μ) := by - calc ∫⁻ (a : α), (f * g) a ∂μ = ∫⁻ (a : α), (f * g) a ∂μ := rfl - _ ≤ ∫⁻ (a : α), f a * (essSup g μ) ∂μ := by - apply MeasureTheory.lintegral_mono_ae - rw [Filter.eventually_iff, ← Filter.exists_mem_subset_iff] - use {a | g a ≤ essSup g μ} - rw [← Filter.eventually_iff] - exact ⟨ae_le_essSup _, by simp; intro _ ha; exact ENNReal.mul_left_mono ha⟩ - _ = (∫⁻ (a : α), f a ∂μ) * (essSup g μ) := by - rw [lintegral_mul_const'' _ hf] +lemma _root_.ENNReal.lintegral_mul_le_one_top (μ : Measure α) {f g : α → ℝ≥0∞} + (hf : AEMeasurable f μ) : ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ∂μ) * (essSup g μ) := by + calc ∫⁻ (a : α), (f * g) a ∂μ = ∫⁻ (a : α), (f * g) a ∂μ := rfl + _ ≤ ∫⁻ (a : α), f a * (essSup g μ) ∂μ := by + apply MeasureTheory.lintegral_mono_ae + rw [Filter.eventually_iff, ← Filter.exists_mem_subset_iff] + use {a | g a ≤ essSup g μ} + rw [← Filter.eventually_iff] + exact ⟨ae_le_essSup _, fun _ ha ↦ ENNReal.mul_left_mono ha⟩ + _ = (∫⁻ (a : α), f a ∂μ) * (essSup g μ) := by + rw [lintegral_mul_const'' _ hf] lemma _root_.ENNReal.lintegral_norm_mul_le_one_top (μ : Measure α) {f : α → E₁} {g : α → E₂} (hf : AEMeasurable f μ) : ∫⁻ a, ‖f a‖₊ * ‖g a‖₊ ∂μ ≤ snorm f 1 μ * snorm g ⊤ μ := by @@ -178,9 +178,7 @@ theorem lintegral_mul_le (hpq : p.IsConjExponent q) (μ : Measure α) {f : α simp only [Pi.mul_apply, coe_mul, implies_true] _ ≤ snorm f p μ * snorm g q μ := by simp only [coe_mul, snorm, coe_eq_zero, coe_ne_top, ↓reduceIte, coe_toReal, mul_ite, mul_zero, ite_mul, zero_mul, hpq.ne_zero, hpq.symm.ne_zero, snorm'] - apply ENNReal.lintegral_mul_le_Lp_mul_Lq _ (NNReal.isConjExponent_coe.mpr hpq) - . apply hf.ennnorm - . apply hg.ennnorm + exact ENNReal.lintegral_mul_le_Lp_mul_Lq _ (NNReal.isConjExponent_coe.mpr hpq) hf.ennnorm hg.ennnorm case one => exact lintegral_norm_mul_le_one_top _ hf case infty => calc From f8ae938215adb92664c80c19642e9390c8fe4951 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 22 Jul 2024 10:38:10 +0200 Subject: [PATCH 10/16] Update Dual.lean --- BonnAnalysis/Dual.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/BonnAnalysis/Dual.lean b/BonnAnalysis/Dual.lean index 6e1b2ff..fef4c28 100644 --- a/BonnAnalysis/Dual.lean +++ b/BonnAnalysis/Dual.lean @@ -260,9 +260,7 @@ lemma q_ne_zero : q ≠ 0 := right_ne_zero hpq.out lemma q_ne_zero' (hqᵢ : q ≠ ∞) : q.toReal ≠ 0 := toReal_ne_zero.mpr ⟨q_ne_zero (p := p), hqᵢ⟩ -lemma q_gt_zero : q > 0 := by - calc q ≥ 1 := hq.out - _ > 0 := p_gt_zero +lemma q_gt_zero : q > 0 := p_gt_zero lemma q_gt_zero' (hqᵢ : q ≠ ∞) : q.toReal > 0 := (toReal_pos_iff_ne_top q).mpr hqᵢ From 467cb1a4a39875bda916eb0dcebf97722c76cb10 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 22 Jul 2024 10:45:10 +0200 Subject: [PATCH 11/16] Update Dual.lean --- BonnAnalysis/Dual.lean | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/BonnAnalysis/Dual.lean b/BonnAnalysis/Dual.lean index fef4c28..357546d 100644 --- a/BonnAnalysis/Dual.lean +++ b/BonnAnalysis/Dual.lean @@ -310,7 +310,7 @@ lemma q_div_p_add_one : q / p + 1 = q := by lemma q_div_p_add_one' (hqᵢ : q ≠ ∞) : q.toReal / p.toReal + 1 = q.toReal := by calc _ = (q / p).toReal + 1 := by rw [toReal_div] - _ = (q / p + 1).toReal := by rw [toReal_add]; simp; exact q_div_p_ne_top hqᵢ; simp + _ = (q / p + 1).toReal := by rw [toReal_add, one_toReal]; apply q_div_p_ne_top hqᵢ; simp _ = q.toReal := by rw [q_div_p_add_one] lemma q_div_p_add_one'' (hqᵢ : q ≠ ∞) : q.toReal / p.toReal = q.toReal - 1 := by @@ -335,8 +335,8 @@ theorem snorm'_mul_const {p : ℝ} (hp : p > 0) (f : α → ℝ) (c : ℝ) : pattern (_ * _) ^ _ rw [ENNReal.mul_rpow_of_ne_top] rfl - apply coe_ne_top - apply coe_ne_top + · exact coe_ne_top + · exact coe_ne_top rw [lintegral_mul_const'] case neg.hr => simp_all @@ -351,8 +351,7 @@ theorem snorm'_mul_const {p : ℝ} (hp : p > 0) (f : α → ℝ) (c : ℝ) : apply ENNReal.rpow_rpow_inv linarith -theorem nnnorm_toReal_eq_abs (x : ℝ) : ‖x‖₊.toReal = |x| := by - rw [coe_nnnorm, norm_eq_abs] +theorem nnnorm_toReal_eq_abs (x : ℝ) : ‖x‖₊.toReal = |x| := by rw [coe_nnnorm, norm_eq_abs] def step' : ℝ → ℝ := Set.piecewise {x | x ≤ 0} 0 1 From 210e863ddb2c975c9cc43f686d269052165b9848 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 22 Jul 2024 10:47:07 +0200 Subject: [PATCH 12/16] Update Dual.lean --- BonnAnalysis/Dual.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/BonnAnalysis/Dual.lean b/BonnAnalysis/Dual.lean index 357546d..848c721 100644 --- a/BonnAnalysis/Dual.lean +++ b/BonnAnalysis/Dual.lean @@ -399,10 +399,7 @@ theorem Real.self_mul_sign (x : ℝ) : x * x.sign = |x| := by . rw [hx₁, Real.sign_zero, mul_zero, abs_zero] . by_cases hx₂ : x > 0 . rw [Real.sign_of_pos hx₂, mul_one, abs_of_pos hx₂] - . have hx₃ : x < 0 := by - apply lt_of_le_of_ne - linarith - exact hx₁ + . have hx₃ : x < 0 := lt_of_le_of_ne (by linarith) hx₁ rw [Real.sign_of_neg hx₃, mul_neg_one, abs_of_neg hx₃] theorem rpow_of_nnnorm_of_sign (x y : ℝ) (hypos : y > 0) From 4f64a7a633efbcdcf874761e8dd2b4092b93ed6b Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 22 Jul 2024 10:49:23 +0200 Subject: [PATCH 13/16] Update Dual.lean --- BonnAnalysis/Dual.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/BonnAnalysis/Dual.lean b/BonnAnalysis/Dual.lean index 848c721..cefb5f3 100644 --- a/BonnAnalysis/Dual.lean +++ b/BonnAnalysis/Dual.lean @@ -419,7 +419,7 @@ theorem ennreal_rpow_of_nnreal' (x : ℝ≥0) (y : ℝ) (hynneg : y ≥ 0) : ENNReal.rpow x y = ofNNReal (NNReal.rpow x y) := by apply (ENNReal.toNNReal_eq_toNNReal_iff' _ _).mp <;> simp . rw [←ENNReal.toNNReal_rpow, ENNReal.toNNReal_coe] - . intro _; assumption + . exact fun _ ↦ hynneg theorem measurable_rpow'_const (c : ℝ) : Measurable (rpow' c) := Measurable.pow (f := fun x => x) (g := fun _ => c) measurable_id measurable_const @@ -437,8 +437,8 @@ theorem rpow_div_eq_one_iff (x : ℝ≥0∞) (y : ℝ) (hy : y > 0) : x^(1/y) = rw [rpow_eq_one_iff x (1/y) this] lemma toNNReal_of_norm_eq_nnnorm (x : ℝ) : ‖x‖.toNNReal = ‖x‖₊ := by - calc _ = ‖‖x‖‖₊ := by apply toNNReal_eq_nnnorm_of_nonneg; apply norm_nonneg - _ = _ := by simp + calc _ = ‖‖x‖‖₊ := toNNReal_eq_nnnorm_of_nonneg (norm_nonneg _) + _ = _ := nnnorm_norm x theorem mul_of_ae_eq {f f' g g' : α → ℝ≥0∞} (hf : f =ᵐ[μ] f') (hg : g =ᵐ[μ] g') : f * g =ᵐ[μ] f' * g' := by From 01a2162b4e92c7db25f49e1cac37ef9d97479435 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 22 Jul 2024 10:54:06 +0200 Subject: [PATCH 14/16] Update Dual.lean --- BonnAnalysis/Dual.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/BonnAnalysis/Dual.lean b/BonnAnalysis/Dual.lean index cefb5f3..f5f5665 100644 --- a/BonnAnalysis/Dual.lean +++ b/BonnAnalysis/Dual.lean @@ -523,8 +523,7 @@ theorem int_conj_q_lt_top'_mul_self (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} rw [mul_assoc, mul_comm, mul_assoc] congr rfl - rw [Real.self_mul_sign] - rw [←nnnorm_toReal_eq_abs] + rw [Real.self_mul_sign, ← nnnorm_toReal_eq_abs] rfl sorry From 2bdbfde38a92c5fe4a982f6d9f0a2e76db944994 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 22 Jul 2024 11:01:29 +0200 Subject: [PATCH 15/16] Update Dual.lean --- BonnAnalysis/Dual.lean | 31 +++++++++++-------------------- 1 file changed, 11 insertions(+), 20 deletions(-) diff --git a/BonnAnalysis/Dual.lean b/BonnAnalysis/Dual.lean index f5f5665..9901755 100644 --- a/BonnAnalysis/Dual.lean +++ b/BonnAnalysis/Dual.lean @@ -642,9 +642,9 @@ def conj_q_lt_top (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) : Lp ℝ p μ := @[simp] theorem snorm_of_conj_q_lt_top (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) : snorm (conj_q_lt_top (p := p) hqᵢ g) p μ = (snorm g q μ) ^ (q.toReal - 1) := by - apply _root_.trans; show _ = snorm (conj_q_lt_top' g) p μ; swap - · exact snorm_of_conj_q_lt_top' hqᵢ g + apply _root_.trans · exact snorm_congr_ae (coeFn_toLp _ ) + · exact snorm_of_conj_q_lt_top' hqᵢ g @[simp] theorem norm_of_conj_q_lt_top (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) @@ -662,7 +662,7 @@ end conj_q_lt_top' section normalized_conj_q_lt_top' def normalized_conj_q_lt_top' {q : ℝ≥0∞} (g : Lp ℝ q μ) : α → ℝ := - fun x => (conj_q_lt_top' g x) * (rpow' (1 - q.toReal) ‖g‖₊) + fun x ↦ (conj_q_lt_top' g x) * (rpow' (1 - q.toReal) ‖g‖₊) @[measurability] theorem normalized_conj_q_lt_top'_ae_measurable (g : Lp ℝ q μ) @@ -680,14 +680,8 @@ theorem normalized_conj_q_lt_top'_aestrongly_measurable (g : Lp ℝ q μ) theorem snorm'_normalized_conj_q_lt_top' {g : Lp ℝ q μ} (hqᵢ : q ≠ ∞) (hg : ‖g‖₊ ≠ 0) : snorm' (normalized_conj_q_lt_top' g) p.toReal μ = 1 := by unfold normalized_conj_q_lt_top' - rw [rpow', snorm'_mul_const p_gt_zero', - snorm'_of_conj_q_lt_top' hqᵢ, - NNReal.rpow_eq_pow, - coe_rpow, - coe_nnnorm, - ←snorm_eq_snorm', - norm_def, - ←neg_sub q.toReal] + rw [rpow', snorm'_mul_const p_gt_zero', snorm'_of_conj_q_lt_top' hqᵢ, NNReal.rpow_eq_pow, + coe_rpow, coe_nnnorm, ← snorm_eq_snorm', norm_def, ← neg_sub q.toReal] case hp_ne_zero => exact q_ne_zero (p := p) case hp_ne_top => exact hqᵢ @@ -696,7 +690,7 @@ theorem snorm'_normalized_conj_q_lt_top' {g : Lp ℝ q μ} (hqᵢ : q ≠ ∞) ( have y_pos : y > 0 := by calc _ = q.toReal - 1 := by rw [hy] - _ > 1 - 1 := by gcongr; apply q_gt_one' (p := p) hqᵢ + _ > 1 - 1 := by gcongr; exact q_gt_one' (p := p) hqᵢ _ = 0 := by ring have y_nneg : y ≥ 0 := by linarith[y_pos] @@ -711,12 +705,11 @@ theorem snorm'_normalized_conj_q_lt_top' {g : Lp ℝ q μ} (hqᵢ : q ≠ ∞) ( have x_rpow_y_ne_top : x^y ≠ ∞ := ENNReal.rpow_ne_top_of_nonneg y_nneg x_ne_top - rw [←ENNReal.coe_toNNReal (a := x ^ y) x_rpow_y_ne_top, + rw [← ENNReal.coe_toNNReal (a := x ^ y) x_rpow_y_ne_top, ENNReal.toReal_rpow, ENNReal.nnnorm_of_toReal_eq_toNNReal] norm_cast - rw [←ENNReal.toNNReal_mul, - ←ENNReal.one_toNNReal] + rw [← ENNReal.toNNReal_mul, ← ENNReal.one_toNNReal] congr rw [←ENNReal.rpow_add] . simp @@ -733,10 +726,9 @@ theorem snorm_normalized_conj_q_lt_top' (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} (h theorem Memℒp_normalized_conj_q_lt_top' (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} (hg : ‖g‖₊ ≠ 0) : Memℒp (normalized_conj_q_lt_top' g) p μ := by - constructor - . exact normalized_conj_q_lt_top'_aestrongly_measurable g - . rw [snorm_normalized_conj_q_lt_top' hqᵢ hg] - trivial + refine ⟨normalized_conj_q_lt_top'_aestrongly_measurable g, ?_⟩ + rw [snorm_normalized_conj_q_lt_top' hqᵢ hg] + trivial def normalized_conj_q_lt_top (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} (hg : ‖g‖₊ ≠ 0) : Lp ℝ p μ := toLp (normalized_conj_q_lt_top' g) (Memℒp_normalized_conj_q_lt_top' hqᵢ hg) @@ -745,7 +737,6 @@ def normalized_conj_q_lt_top (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} (hg : ‖g‖ theorem snorm_normalized_conj_q_lt_top (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} (hg : ‖g‖₊ ≠ 0) : snorm (normalized_conj_q_lt_top (p := p) hqᵢ hg) p μ = 1 := by apply _root_.trans - show _ = snorm (normalized_conj_q_lt_top' g) p μ; · exact snorm_congr_ae (coeFn_toLp _) · exact snorm_normalized_conj_q_lt_top' hqᵢ hg From 8ad2e67c9fd4663ac9c41139e6ccfe050d97b168 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 14 Aug 2024 15:28:30 +0000 Subject: [PATCH 16/16] Fix minor errors --- BonnAnalysis/ComplexInterpolation.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/BonnAnalysis/ComplexInterpolation.lean b/BonnAnalysis/ComplexInterpolation.lean index e750ef1..91b006c 100644 --- a/BonnAnalysis/ComplexInterpolation.lean +++ b/BonnAnalysis/ComplexInterpolation.lean @@ -41,9 +41,8 @@ lemma Real.le_one_of_add_nonneg_eq_one {t s : ℝ} (hs : 0 ≤ s) (hts : t + s = calc t = 1 - s := eq_sub_of_add_eq hts _ ≤ 1 := by simp [hs] -} -lemma pow_bound₀ {M:ℝ} (hM: M > 0) {z: ℂ} (hz: z.re ∈ Icc 0 1) : Complex.abs (M^(z-1)) ≤ max 1 (1/M) := by{ +lemma pow_bound₀ {M:ℝ} (hM: M > 0) {z: ℂ} (hz: z.re ∈ Icc 0 1) : Complex.abs (M^(z-1)) ≤ max 1 (1/M) := by rw [Complex.abs_cpow_eq_rpow_re_of_pos hM (z-1)] simp simp at hz @@ -711,7 +710,7 @@ theorem DiffContOnCl.norm_le_pow_mul_pow {a b : ℝ} {f : ℂ → ℂ} (hab: a