From 6b486ac47bdd7a81d9e5b659d0e7f81ae360fa39 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Thu, 15 Aug 2024 11:11:49 +0000 Subject: [PATCH] Golf a few proofs (#42) --- BonnAnalysis/ComplexInterpolation.lean | 347 ++++++++----------------- BonnAnalysis/Dual.lean | 119 ++++----- 2 files changed, 159 insertions(+), 307 deletions(-) diff --git a/BonnAnalysis/ComplexInterpolation.lean b/BonnAnalysis/ComplexInterpolation.lean index ff83944..91b006c 100644 --- a/BonnAnalysis/ComplexInterpolation.lean +++ b/BonnAnalysis/ComplexInterpolation.lean @@ -37,13 +37,12 @@ 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] -} -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 @@ -52,23 +51,15 @@ lemma pow_bound₀ {M:ℝ} (hM: M > 0) {z: ℂ} (hz: z.re ∈ Icc 0 1) : Complex 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 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 - constructor - · simp at h; exact le_of_lt h - · exact 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{ @@ -82,27 +73,19 @@ 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 - constructor - · exact h - · 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 - constructor - · simp at h; exact le_of_lt h - · exact hz.2 + exact this (Or.inr ⟨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] @@ -115,43 +98,30 @@ lemma abs_fun_bounded {f:ℂ → ℂ} (h2f : IsBounded (f '' { z | z.re ∈ Icc } /- 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] -} -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] -} - -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] 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 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 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, 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,24 +137,16 @@ 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{ @@ -192,17 +154,14 @@ theorem DiffContOnCl.norm_le_pow_mul_pow''' {f : ℂ → ℂ} · have : norm ∘ f = (fun z ↦ Complex.abs (f z) ) := by rfl 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 + · simp only [mem_Icc, tendsto_map'_iff, hzu] exact hu2 } rw [Filter.disjoint_iff] at this @@ -214,13 +173,11 @@ theorem DiffContOnCl.norm_le_pow_mul_pow''' {f : ℂ → ℂ} 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 + 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 [mem_principal] at hA₂ + 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 @@ -230,17 +187,14 @@ theorem DiffContOnCl.norm_le_pow_mul_pow''' {f : ℂ → ℂ} _ ⊆ 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' 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' @@ -295,21 +249,17 @@ 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₂⟩ } @@ -327,11 +277,9 @@ theorem DiffContOnCl.norm_le_pow_mul_pow''' {f : ℂ → ℂ} 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] @@ -347,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 @@ -378,8 +326,7 @@ theorem DiffContOnCl.norm_le_pow_mul_pow''' {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 } @@ -388,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] @@ -421,26 +361,19 @@ 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] - 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 - } -} - + rw [Real.exp_le_one_iff, mul_nonpos_iff] + 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 + 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] @@ -470,15 +403,12 @@ 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] - left - constructor - · exact le_of_lt hε - · simp - calc - -1 ≤ 0 := by norm_num - _ ≤ y^2 := sq_nonneg y + rw [Real.exp_le_one_iff, mul_nonpos_iff] + refine Or.inl ⟨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 @@ -495,10 +425,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 @@ -561,10 +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 - constructor - · exact le_of_lt hε - · 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 @@ -609,52 +533,34 @@ lemma perturb_vanish_infty {f:ℂ → ℂ} (h2f : IsBounded (f '' { z | z.re ∈ · 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{ +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] 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 -} - + 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{ +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 : ℂ → ℂ} @@ -667,21 +573,17 @@ theorem DiffContOnCl.norm_le_pow_mul_pow'' {f : ℂ → ℂ} apply @le_of_tendsto _ _ _ _ _ (fun ε ↦ Complex.abs (perturb f ε (t + I * y))) _ _ _ _ this 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} @@ -758,9 +660,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₂] @@ -807,10 +709,7 @@ theorem DiffContOnCl.norm_le_pow_mul_pow {a b : ℝ} {f : ℂ → ℂ} (hab: a exact lintegral_norm_mul_le_one_top _ hf case infty => calc @@ -219,7 +217,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 @@ -268,9 +266,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ᵢ @@ -280,22 +276,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ᵢ) @@ -314,13 +303,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] @@ -356,8 +343,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 only [ne_eq, rpow_eq_top_iff, ENNReal.coe_eq_zero, nnnorm_eq_zero, @@ -375,8 +362,7 @@ theorem snorm'_mul_const {p : ℝ} (hp : p > 0) (f : α → ℝ) (c : ℝ) : apply ENNReal.rpow_rpow_inv exact ne_of_gt hp -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 @@ -424,10 +410,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) @@ -447,7 +430,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 @@ -465,8 +448,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 @@ -495,9 +478,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 @@ -507,9 +489,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 @@ -573,8 +555,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 have hq' : q ≠ 0 := by { @@ -715,9 +696,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 μ) @@ -735,7 +716,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 μ) @@ -754,16 +735,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' - unfold rpow' - - rw [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ᵢ @@ -772,27 +745,26 @@ 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] - 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 - 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 @@ -803,16 +775,15 @@ 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 - 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) @@ -821,9 +792,8 @@ 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 · 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) @@ -867,12 +837,11 @@ 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 only [Set.mem_setOf_eq] 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 _ = ‖f‖ * ‖g‖ := by rw [opNorm_mul, one_mul]