From 0ba357e18157bf100b8445ab919c150a56acb83e Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Thu, 21 Nov 2024 16:08:59 +0100 Subject: [PATCH] chore: bump (v4.14.0-rc2) (#182) - [x] Remove `_root_.ENNReal.inv_div` since upstreamed to Mathlib https://github.com/leanprover-community/mathlib4/pull/18704 - [x] Remove `Int.floor_le_iff` since upstreamed to Mathlib https://github.com/leanprover-community/mathlib4/pull/18552 - [x] Remove `dense_iff_iUnion_ball` since upstreamed to Mathlib https://github.com/leanprover-community/mathlib4/pull/19294 - [x] Remove `dist_eq_of_dist_zero` since upstreamed to Mathlib https://github.com/leanprover-community/mathlib4/pull/19294 - [x] Remove `IsTop.isMax_iff` since upstreamed to Mathlib https://github.com/leanprover-community/mathlib4/pull/19305 - [x] Remove `Int.Icc_of_eq_sub_one` since upstreamed to Mathlib https://github.com/leanprover-community/mathlib4/pull/19308 --------- Co-authored-by: grunweg --- Carleson/Antichain/AntichainOperator.lean | 2 +- Carleson/Classical/Basic.lean | 2 +- Carleson/Classical/VanDerCorput.lean | 2 +- Carleson/Discrete/ForestUnion.lean | 2 +- Carleson/ForestOperator/LargeSeparation.lean | 2 +- Carleson/ForestOperator/RemainingTiles.lean | 6 +- Carleson/HardyLittlewood.lean | 8 +- Carleson/Psi.lean | 15 +-- Carleson/RealInterpolation.lean | 103 +++++++------------ Carleson/ToMathlib/ENorm.lean | 15 +-- Carleson/ToMathlib/Misc.lean | 46 +-------- lake-manifest.json | 22 ++-- lakefile.toml | 1 - lean-toolchain | 2 +- 14 files changed, 78 insertions(+), 150 deletions(-) diff --git a/Carleson/Antichain/AntichainOperator.lean b/Carleson/Antichain/AntichainOperator.lean index 19a8719f..dd96d26b 100644 --- a/Carleson/Antichain/AntichainOperator.lean +++ b/Carleson/Antichain/AntichainOperator.lean @@ -486,7 +486,7 @@ lemma Dens2Antichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤·) ( apply Nat.le_mul_of_pos_right _ rw [tsub_pos_iff_lt] exact lt_of_lt_of_le (by linarith) - (Nat.mul_le_mul_left 4 (pow_le_pow_left zero_le_four ha 2)) + (Nat.mul_le_mul_left 4 (pow_le_pow_left₀ zero_le_four ha 2)) _ = 4 * a ^ 3 - 2 * a := by rw [Nat.mul_sub] ring_nf diff --git a/Carleson/Classical/Basic.lean b/Carleson/Classical/Basic.lean index 442db40e..4e1496ae 100644 --- a/Carleson/Classical/Basic.lean +++ b/Carleson/Classical/Basic.lean @@ -208,7 +208,7 @@ lemma lower_secant_bound {η : ℝ} {x : ℝ} (xIcc : x ∈ Set.Icc (-2 * π + rw [mul_assoc] gcongr field_simp - rw [div_le_div_iff (by norm_num) pi_pos] + rw [div_le_div_iff₀ (by norm_num) pi_pos] linarith [pi_le_four] _ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by apply lower_secant_bound' xAbs diff --git a/Carleson/Classical/VanDerCorput.lean b/Carleson/Classical/VanDerCorput.lean index ec5653d7..c2b3e527 100644 --- a/Carleson/Classical/VanDerCorput.lean +++ b/Carleson/Classical/VanDerCorput.lean @@ -208,7 +208,7 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B linarith _ ≤ (2 * π / (1 + n * (b - a)) * (b - a)) * (B + K * (b - a) / 2) := by gcongr - rw [mul_comm, ← mul_div_assoc, div_le_div_iff (by simpa)] + rw [mul_comm, ← mul_div_assoc, div_le_div_iff₀ (by simpa)] · calc π * (1 + n * (b - a)) _ ≤ π * (π + n * (b - a)) := by gcongr diff --git a/Carleson/Discrete/ForestUnion.lean b/Carleson/Discrete/ForestUnion.lean index 313e4c46..733d5260 100644 --- a/Carleson/Discrete/ForestUnion.lean +++ b/Carleson/Discrete/ForestUnion.lean @@ -400,7 +400,7 @@ lemma forest_separation (hu : u ∈ 𝔘₃ k n j) (hu' : u' ∈ 𝔘₃ k n j) have Cidpos : 0 < (C2_1_2 a)⁻¹ ^ d := by rw [C2_1_2]; positivity calc _ ≤ (C2_1_2 a)⁻¹ ^ (Z * (n + 1)) := by - refine pow_le_pow_left zero_le_two ?_ _ + refine pow_le_pow_left₀ zero_le_two ?_ _ nth_rw 1 [C2_1_2, ← Real.inv_rpow zero_le_two, ← Real.rpow_neg_one, ← Real.rpow_mul zero_le_two, neg_one_mul, neg_mul, neg_neg, ← Real.rpow_one 2] apply Real.rpow_le_rpow_of_exponent_le one_le_two diff --git a/Carleson/ForestOperator/LargeSeparation.lean b/Carleson/ForestOperator/LargeSeparation.lean index d78fc45e..185b34d8 100644 --- a/Carleson/ForestOperator/LargeSeparation.lean +++ b/Carleson/ForestOperator/LargeSeparation.lean @@ -166,7 +166,7 @@ lemma scales_impacting_interval (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : apply Grid_subset_ball (X := X) (i := 𝓘 p) exact xInTile _ < 100 * ↑D ^ (s J + 1) := by - apply (div_lt_div_right zero_lt_four).mp + apply (div_lt_div_iff_of_pos_right zero_lt_four).mp ring_nf rewrite (config := {occs := .pos [1]}) [add_comm] apply lt_tsub_iff_left.mp diff --git a/Carleson/ForestOperator/RemainingTiles.lean b/Carleson/ForestOperator/RemainingTiles.lean index cee3139e..e76e7922 100644 --- a/Carleson/ForestOperator/RemainingTiles.lean +++ b/Carleson/ForestOperator/RemainingTiles.lean @@ -87,7 +87,11 @@ lemma square_function_count (hJ : J ∈ 𝓙₆ t u₁) (s' : ℤ) : · rw [show (8 : ℝ≥0) = 2 ^ 3 by norm_num] simp only [defaultD, Nat.cast_pow, Nat.cast_ofNat, defaultA, ← zpow_neg, ← zpow_natCast, ← zpow_mul, ← zpow_add₀ (show (2 : ℝ≥0) ≠ 0 by norm_num)] - gcongr + -- #adaptation note(2024-11-02): this line was `gcongr` + -- This was probably broken by mathlib4#19626 and friends, see + -- https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/.2319314.20adaptations.20for.20nightly-2024-11-20 + -- for details. + refine zpow_le_zpow_right₀ ?ha ?hmn · norm_num · simp only [Nat.cast_mul, Nat.cast_ofNat, Nat.cast_pow, mul_neg, le_add_neg_iff_add_le, ← mul_add] diff --git a/Carleson/HardyLittlewood.lean b/Carleson/HardyLittlewood.lean index 126437bc..6a8813d8 100644 --- a/Carleson/HardyLittlewood.lean +++ b/Carleson/HardyLittlewood.lean @@ -232,18 +232,18 @@ theorem Set.Countable.measure_biUnion_le_lintegral [OpensMeasurableSpace X] (h hB (Subtype.coe_prop i) (Subtype.coe_prop j) (Subtype.coe_ne_coe.mpr hij) calc l * μ (⋃ i ∈ 𝓑, ball (c i) (r i)) ≤ l * μ (⋃ i ∈ B, ball (c i) (2 ^ 2 * r i)) := by - refine l.mul_left_mono (μ.mono fun x hx ↦ ?_) + refine mul_left_mono (μ.mono fun x hx ↦ ?_) simp only [mem_iUnion, mem_ball, exists_prop] at hx rcases hx with ⟨i, i𝓑, hi⟩ obtain ⟨b, bB, hb⟩ := h2B i i𝓑 refine mem_iUnion₂.mpr ⟨b, bB, hb <| mem_ball.mpr hi⟩ _ ≤ l * ∑' i : B, μ (ball (c i) (2 ^ 2 * r i)) := - l.mul_left_mono <| measure_biUnion_le μ (h𝓑.mono hB𝓑) fun i ↦ ball (c i) (2 ^ 2 * r i) + mul_left_mono <| measure_biUnion_le μ (h𝓑.mono hB𝓑) fun i ↦ ball (c i) (2 ^ 2 * r i) _ ≤ l * ∑' i : B, A ^ 2 * μ (ball (c i) (r i)) := by - refine l.mul_left_mono <| ENNReal.tsum_le_tsum (fun i ↦ ?_) + refine mul_left_mono <| ENNReal.tsum_le_tsum (fun i ↦ ?_) rw [sq, sq, mul_assoc, mul_assoc] apply (measure_ball_two_le_same (c i) (2 * r i)).trans - exact ENNReal.mul_left_mono (measure_ball_two_le_same (c i) (r i)) + exact mul_left_mono (measure_ball_two_le_same (c i) (r i)) _ = A ^ 2 * ∑' i : B, l * μ (ball (c i) (r i)) := by rw [ENNReal.tsum_mul_left, ENNReal.tsum_mul_left, ← mul_assoc, ← mul_assoc, mul_comm l] _ ≤ A ^ 2 * ∑' i : B, ∫⁻ x in ball (c i) (r i), u x ∂μ := by diff --git a/Carleson/Psi.lean b/Carleson/Psi.lean index 7000d0da..b5cb24d9 100644 --- a/Carleson/Psi.lean +++ b/Carleson/Psi.lean @@ -229,7 +229,10 @@ private lemma sum_ψ₂ (hx : 0 < x) have endpts := endpoint_sub_one hD hx h have ne : ⌈logb D (4 * x)⌉ - 1 ≠ ⌈logb D (4 * x)⌉ := pred_ne_self _ have : nonzeroS D x = {⌈logb D (4 * x)⌉ - 1, ⌈logb D (4 * x)⌉} := by - rw [nonzeroS, ← endpts]; exact Int.Icc_of_eq_sub_1 endpts + rw [nonzeroS, ← endpts] + have Icc_of_eq_add_one {a b : ℤ} (h : a + 1 = b) : Finset.Icc a b = {a, b} := by + subst h; exact Int.Icc_eq_pair a + exact Icc_of_eq_add_one (add_eq_of_eq_sub endpts) set s₀ := ⌈logb D (4 * x)⌉ rw [this, Finset.sum_insert ((Finset.not_mem_singleton).2 ne), Finset.sum_singleton] -- Now calculate the sum @@ -259,7 +262,7 @@ lemma mem_nonzeroS_iff {i : ℤ} {x : ℝ} (hx : 0 < x) : i ∈ nonzeroS D x ↔ (D ^ (-i) * x) ∈ Ioo (4 * D : ℝ)⁻¹ 2⁻¹ := by rw [mem_Ioo, nonzeroS, Finset.mem_Icc, Int.floor_le_iff, Int.le_ceil_iff, mul_inv_rev, add_comm _ 1, Real.add_lt_add_iff_left, ← lt_div_iff₀ hx, mul_comm (D : ℝ)⁻¹, - ← div_lt_div_iff hx (inv_pos.2 (D0 hD)), div_inv_eq_mul, ← zpow_add_one₀ ((D0 hD).ne.symm), + ← div_lt_div_iff₀ hx (inv_pos.2 (D0 hD)), div_inv_eq_mul, ← zpow_add_one₀ ((D0 hD).ne.symm), zpow_neg, ← Real.rpow_intCast, ← Real.rpow_intCast, lt_logb_iff_rpow_lt hD (four_x0 hx), logb_lt_iff_lt_rpow hD (mul_pos two_pos hx), ← sub_eq_neg_add, ← neg_sub i 1, ← inv_mul', ← inv_mul', inv_lt_inv₀ (D_pow0 hD _) (mul_pos two_pos hx), Int.cast_neg, Int.cast_sub, @@ -406,10 +409,10 @@ private lemma div_vol_le {x y : X} {c : ℝ} (hc : c > 0) (hK : Ks s x y ≠ 0) have v0₂ := measure_ball_pos_nnreal x (D ^ (s - 1) / 4) (by have := D0' X; positivity) have v0₃ := measure_ball_pos_real x (D ^ s) (zpow_pos (D0' X) _) have ball_subset := ball_subset_ball (x := x) (mem_Icc.1 (dist_mem_Icc_of_Ks_ne_zero hK)).1 - apply le_trans <| (div_le_div_left hc v0₁ v0₂).2 <| + apply le_trans <| (div_le_div_iff_of_pos_left hc v0₁ v0₂).2 <| ENNReal.toNNReal_mono (measure_ball_ne_top x _) (OuterMeasureClass.measure_mono _ ball_subset) dsimp only - rw_mod_cast [measureNNReal_val, div_le_div_iff (by exact_mod_cast v0₂) v0₃] + rw_mod_cast [measureNNReal_val, div_le_div_iff₀ (by exact_mod_cast v0₂) v0₃] apply le_of_le_of_eq <| (mul_le_mul_left hc).2 <| DoublingMeasure.volume_ball_two_le_same_repeat' s x simp_rw [defaultA, ← mul_assoc, mul_comm c] @@ -599,11 +602,11 @@ private lemma norm_Ks_sub_Ks_le₁ {s : ℤ} {x y y' : X} (hK : Ks s x y ≠ 0) apply le_trans <| norm_sub_le (Ks s x y) (Ks s x y') apply le_trans <| add_le_add norm_Ks_le norm_Ks_le rw [div_mul_eq_mul_div, div_add_div_same, ← two_mul, - div_le_div_right (measure_ball_pos_real x (D ^ s) (D_pow0' (D1 X) s)), ← pow_one 2] + div_le_div_iff_of_pos_right (measure_ball_pos_real x (D ^ s) (D_pow0' (D1 X) s)), ← pow_one 2] rw [not_le, ← div_lt_iff₀' two_pos] at h have dist_pos : dist y y' > 0 := lt_of_le_of_lt (div_nonneg dist_nonneg two_pos.le) h have := lt_of_le_of_lt - ((div_le_div_right two_pos).2 ((mem_Icc.1 <| dist_mem_Icc_of_Ks_ne_zero hK).1)) h + ((div_le_div_iff_of_pos_right two_pos).2 ((mem_Icc.1 <| dist_mem_Icc_of_Ks_ne_zero hK).1)) h rw [div_div, (show (4 : ℝ) * 2 = 8 by norm_num), zpow_sub₀ (D0' X).ne.symm, div_div, zpow_one, div_lt_comm₀ (by positivity) dist_pos] at this have dist_div_Ds_gt := inv_strictAnti₀ (div_pos (Ds0 X s) dist_pos) this diff --git a/Carleson/RealInterpolation.lean b/Carleson/RealInterpolation.lean index d920919e..0183ef84 100644 --- a/Carleson/RealInterpolation.lean +++ b/Carleson/RealInterpolation.lean @@ -402,8 +402,7 @@ lemma ζ_equality₁ (ht : t ∈ Ioo 0 1) : (((1 - t) * q₀⁻¹.toReal + t * q₁⁻¹.toReal) * ((1 - t) * p₀⁻¹.toReal + t * p₁⁻¹.toReal - p₀⁻¹.toReal)) := by unfold ζ - have t_pos : 0 < t := ht.1 - rw [← mul_div_mul_right _ _ t_pos.ne', mul_assoc _ _ t, mul_assoc _ _ t] + rw [← mul_div_mul_right _ _ ht.1.ne', mul_assoc _ _ t, mul_assoc _ _ t] congr <;> ring lemma ζ_equality₂ (ht : t ∈ Ioo 0 1) : @@ -1365,7 +1364,7 @@ def trnc [NormedAddCommGroup E₁] (j : Bool) (f : α → E₁) (t : ℝ) : α /-- A function is the complement if its truncation and the complement of the truncation. -/ lemma trunc_buildup [NormedAddCommGroup E₁] : f = trunc f t + trunc_compl f t := by - ext x; unfold trunc_compl trunc; simp + ext x; simp [trunc, trunc_compl] /-- If the truncation parameter is non-positive, the truncation vanishes. -/ lemma trunc_of_nonpos {f : α → E₁} {a : ℝ} [NormedAddCommGroup E₁] (ha : a ≤ 0) : @@ -1816,8 +1815,7 @@ lemma res_subset_Ioi {j : Bool} {β : ℝ} (hβ : β > 0) : res j β ⊆ Ioi 0 : unfold res split · exact Ioo_subset_Ioi_self - · unfold Ioi - simp only [setOf_subset_setOf] + · simp only [Ioi, setOf_subset_setOf] intro s hs linarith @@ -2059,7 +2057,7 @@ def trunc_cut (f : α → ℝ≥0∞) (μ : Measure α) [SigmaFinite μ] := lemma trunc_cut_mono {μ : Measure α} [SigmaFinite μ] {f : α → ℝ≥0∞} : ∀ x : α, Monotone (fun n ↦ trunc_cut f μ n x) := by - intro x m n hmn; unfold trunc_cut; unfold indicator; simp only + intro x m n hmn; simp only [trunc_cut, indicator] split_ifs with is_fx_le_m is_fx_le_n · refine min_le_min_left (f x) (Nat.cast_le.mpr hmn) · contrapose! is_fx_le_n @@ -2075,8 +2073,7 @@ lemma trunc_cut_mono₀ {μ : Measure α} [SigmaFinite μ] {f : α → ℝ≥0 lemma trunc_cut_sup {μ : Measure α} [SigmaFinite μ] {f : α → ℝ≥0∞} : ∀ x : α, ⨆ n : ℕ, trunc_cut f μ n x = f x := by intro x; refine iSup_eq_of_forall_le_of_forall_lt_exists_gt ?h₁ ?h₂ - · intro n; unfold trunc_cut - unfold indicator + · intro n; unfold trunc_cut indicator split_ifs · exact min_le_left (f x) ↑n · exact zero_le _ @@ -2090,7 +2087,7 @@ lemma trunc_cut_sup {μ : Measure α} [SigmaFinite μ] {f : α → ℝ≥0∞} : rcases this with ⟨m, wm⟩ rcases ENNReal.exists_nat_gt hw.ne_top with ⟨n, wn⟩ use (m + n) - unfold indicator; simp only + simp only [indicator] split_ifs with is_x_in_Ampn · refine lt_min hw ?_ calc @@ -2112,10 +2109,8 @@ lemma representationLp {μ : Measure α} [SigmaFinite μ] {f : α → ℝ≥0∞ let g := trunc_cut f μ have hpq' : p.IsConjExponent q := Real.IsConjExponent.mk hp hpq have f_mul : ∀ n : ℕ, (g n) ^ p ≤ f * (g n) ^ (p - 1) := by - intro n x; unfold_let g; - simp only [Pi.pow_apply, Pi.mul_apply] - unfold trunc_cut - unfold indicator + intro n x + simp only [g, Pi.pow_apply, Pi.mul_apply, trunc_cut, indicator] split_ifs · refine le_trans (b := (min (f x) ↑n) * min (f x) ↑n ^ (p - 1)) ?_ ?_ · nth_rewrite 1 [← add_sub_cancel 1 p] @@ -2135,28 +2130,23 @@ lemma representationLp {μ : Measure α} [SigmaFinite μ] {f : α → ℝ≥0∞ exact trunc_cut_mono _ hmn · exact (g_lim x).ennrpow_const p have g_meas (n : ℕ): AEMeasurable (g n) μ := by - unfold_let g exact AEMeasurable.indicator (by fun_prop) (measurableSet_spanningSets μ n) have g_fin (n : ℕ): ∫⁻ (z : α), g n z ^ p ∂μ < ⊤ := by calc _ = ∫⁻ (z : α) in A n, g n z ^ p ∂μ := by - unfold_let g - unfold trunc_cut + unfold g trunc_cut rw [← lintegral_indicator]; swap; exact measurableSet_spanningSets μ n congr 1 ext x - unfold indicator - dsimp only + dsimp only [indicator] split_ifs · rfl · simp only [ENNReal.rpow_eq_zero_iff, true_and, zero_ne_top, false_and, or_false]; positivity _ ≤ ∫⁻ (_x : α) in A n, n ^ p ∂μ := by apply setLIntegral_mono measurable_const · intro x hx - unfold_let g - unfold trunc_cut gcongr - unfold indicator + unfold g trunc_cut indicator split_ifs · exact min_le_right (f x) ↑n · contradiction @@ -2212,7 +2202,7 @@ lemma representationLp {μ : Measure α} [SigmaFinite μ] {f : α → ℝ≥0∞ apply iSup_le_iSup_of_subset fun r exists_n ↦ ?_ rcases exists_n with ⟨n, wn⟩ simp_rw [← wn] - unfold_let h + unfold h refine ⟨by fun_prop, ?_⟩ simp_rw [div_eq_mul_inv] calc @@ -2382,7 +2372,7 @@ lemma truncation_ton_measurable {f : α → E₁} let A := {(s, x) : ℝ × α | ‖f x‖₊ ≤ tc.ton s} have : (fun z : ℝ × α ↦ (trunc f (tc.ton z.1)) z.2) = Set.indicator A (fun z : ℝ × α ↦ f z.2) := by - ext z; unfold trunc; unfold indicator; unfold_let A; simp + ext z; simp [trunc, indicator, A] rw [this] exact (aemeasurable_indicator_iff₀ (indicator_ton_measurable hf.restrict _)).mpr hf.restrict.snd.restrict @@ -2396,7 +2386,7 @@ lemma truncation_compl_ton_measurable {f : α → E₁} ((volume.restrict (Ioi 0)).prod (μ.restrict (Function.support f) )) := by let A := {(s, x) : ℝ × α | tc.ton s < ‖f x‖₊} have : (fun z : ℝ × α ↦ (f - trunc f (tc.ton z.1)) z.2) = Set.indicator A (fun z : ℝ × α ↦ f z.2) := by - ext z; rw [trunc_compl_eq]; unfold_let A; unfold indicator; simp + ext z; rw [trunc_compl_eq]; simp [A, indicator] rw [this] refine (aemeasurable_indicator_iff₀ (indicator_ton_measurable_lt hf.restrict _)).mpr hf.restrict.snd.restrict @@ -2404,9 +2394,8 @@ lemma truncation_compl_ton_measurable {f : α → E₁} lemma restrict_to_support {a : ℝ} {p : ℝ} (hp : p > 0) [NormedAddCommGroup E₁] (f : α → E₁) : ∫⁻ x : α in Function.support f, ‖trunc f a x‖₊ ^ p ∂ μ = ∫⁻ x : α, ‖trunc f a x‖₊ ^ p ∂μ := by apply setLIntegral_eq_of_support_subset - unfold Function.support + unfold Function.support trunc rw [setOf_subset_setOf] - unfold trunc intro x contrapose! intro f_zero @@ -2417,9 +2406,8 @@ lemma restrict_to_support_trunc_compl {a : ℝ} {p : ℝ} [NormedAddCommGroup E ∫⁻ x : α in Function.support f, ‖(f - trunc f a) x‖₊ ^ p ∂μ = ∫⁻ x : α, ‖(f - trunc f a) x‖₊ ^ p ∂μ := by apply setLIntegral_eq_of_support_subset - unfold Function.support + unfold Function.support trunc rw [setOf_subset_setOf] - unfold trunc intro x contrapose! intro f_zero @@ -2431,9 +2419,8 @@ lemma restrict_to_support_trnc {a : ℝ} {p : ℝ} {j : Bool} [NormedAddCommGrou ∫⁻ x : α in Function.support f, ‖trnc j f a x‖₊ ^ p ∂μ = ∫⁻ x : α, ‖trnc j f a x‖₊ ^ p ∂μ := by apply setLIntegral_eq_of_support_subset - unfold Function.support + unfold Function.support trnc trunc rw [setOf_subset_setOf] - unfold trnc trunc intro x contrapose! intro f_zero @@ -2521,8 +2508,7 @@ lemma estimate_trnc {p₀ q₀ q : ℝ} {spf : ScaledPowerFunction} {j : Bool} (∫⁻ (a : α) in Function.support f, ↑‖trnc j f (tc.ton s) a‖₊ ^ p₀ ∂μ) ^ (p₀⁻¹ * q₀) := by apply setLIntegral_congr_fun measurableSet_Ioi - apply ae_of_all - intro s _ + filter_upwards with s _ rw [ENNReal.rpow_inv_rpow] · rw [one_div, ← ENNReal.rpow_mul, restrict_to_support_trnc hp₀] · positivity @@ -2532,8 +2518,7 @@ lemma estimate_trnc {p₀ q₀ q : ℝ} {spf : ScaledPowerFunction} {j : Bool} ↑‖trnc j f (tc.ton s) a‖₊ ^ p₀ ∂μ) ^ (p₀⁻¹ * q₀) := by apply setLIntegral_congr_fun measurableSet_Ioi - apply ae_of_all - intro s _ + filter_upwards with s _ rw [lintegral_const_mul', ENNReal.mul_rpow_of_nonneg] · positivity · exact (ENNReal.rpow_lt_top_of_nonneg (by positivity) coe_ne_top).ne @@ -2552,8 +2537,7 @@ lemma estimate_trnc {p₀ q₀ q : ℝ} {spf : ScaledPowerFunction} {j : Bool} intro x _ congr 1 apply setLIntegral_congr_fun measurableSet_Ioi - apply ae_of_all - intro s _ + filter_upwards with s _ rw [ENNReal.mul_rpow_of_nonneg, ENNReal.rpow_inv_rpow, ← ENNReal.rpow_mul] <;> try positivity congr field_simp @@ -2590,7 +2574,6 @@ lemma estimate_trnc {p₀ q₀ q : ℝ} {spf : ScaledPowerFunction} {j : Bool} apply lintegral_congr_support hf intro x hfx congr 1 - unfold_let tc apply value_lintegral_res₁ exact norm_pos_iff'.mpr hfx _ = (∫⁻ a : α in Function.support f, @@ -2705,12 +2688,10 @@ lemma estimate_trnc₁ {spf : ScaledPowerFunction} {j : Bool} ext x congr rcases j - · unfold sel - dsimp only + · dsimp only [sel] rw [hspf] apply ζ_equality₅ (hp₀p₁ := hp₀p₁.ne) <;> assumption - · unfold sel - dsimp only + · dsimp only [sel] rw [hspf] apply ζ_equality₆ (hp₀p₁ := hp₀p₁.ne) <;> assumption _ ≤ ENNReal.ofReal (spf.d ^ (q.toReal - (sel j q₀ q₁).toReal)) * @@ -3527,8 +3508,7 @@ lemma support_sigma_finite_from_Memℒp SigmaFinite (μ.restrict (Function.support f)) := by let g : α → ℝ≥0∞ := fun x ↦ ‖f x‖₊ ^ p.toReal have : Function.support g = Function.support f := by - unfold Function.support - unfold_let g + unfold Function.support g ext x simp only [ne_eq, ENNReal.rpow_eq_zero_iff, ENNReal.coe_eq_zero, nnnorm_eq_zero, coe_ne_top, false_and, or_false, not_and, not_lt, mem_setOf_eq] @@ -3540,9 +3520,8 @@ lemma support_sigma_finite_from_Memℒp · tauto rw [← this] apply support_sigma_finite_of_lintegrable - · unfold_let g - exact (hf.1.aemeasurable.nnnorm.coe_nnreal_ennreal).pow_const _ - · unfold_let g + · exact (hf.1.aemeasurable.nnnorm.coe_nnreal_ennreal).pow_const _ + · unfold g have obs := hf.2 unfold eLpNorm eLpNorm' at obs split_ifs at obs @@ -3613,40 +3592,31 @@ lemma combine_estimates₀ {A : ℝ} (hA : A > 0) exact d_eq_top₀ one_le_p₀ q₁pos hp₀p₁.ne_top q₀top hq₀q₁ · exact (interp_exp_between p₀pos p₁pos hp₀p₁ ht hp).1 · exact interp_exp_ne_top hp₀p₁.ne ht hp - · unfold_let tc - unfold spf_to_tc - dsimp only + · dsimp only [tc, spf_to_tc] congr rw [hspf] - unfold spf_ch - dsimp only + dsimp only [spf_ch] exact ζ_equality₇ ht one_le_p₀ q₀pos one_le_p1 q₁pos hp₀p₁.ne hq₀q₁ hp hq hp₀p₁.ne_top q₀top · intro q₁top s (hs : s > 0) rcases (eq_or_ne p₁ ⊤) with p₁eq_top | p₁ne_top · apply weaktype_estimate_trunc_top_top hC₁ _ p₁eq_top q₁top _ hf h₁T hs - · unfold_let tc - unfold spf_to_tc - dsimp only + · dsimp only [tc, spf_to_tc] rw [hspf] - unfold spf_ch - dsimp only + dsimp only [spf_ch] rw [d_eq_top_top] <;> try assumption rw [ζ_eq_top_top, Real.rpow_one] <;> try assumption exact hp₀p₁.ne · exact p_pos · exact (interp_exp_between p₀pos p₁pos hp₀p₁ ht hp).2 · apply weaktype_estimate_trunc_top (p₁ := p₁) (p := p) (d := spf.d) hC₁ <;> try assumption - · unfold_let tc + · unfold tc rw [hspf] - unfold spf_to_tc spf_ch - dsimp only + dsimp only [spf_to_tc, spf_ch] congr apply ζ_equality₈ ht (hp₀p₁ := hp₀p₁.ne) <;> assumption - · unfold_let tc - rw [hspf] - unfold spf_ch - dsimp only + · rw [hspf] + dsimp only [spf_ch] apply d_eq_top₁ <;> assumption · exact p₁ne_top.lt_top · exact (interp_exp_between p₀pos p₁pos hp₀p₁ ht hp).2 @@ -3688,8 +3658,7 @@ lemma combine_estimates₀ {A : ℝ} (hA : A > 0) ENNReal.ofReal (spf.d ^ (q.toReal - q₀.toReal)) * ENNReal.ofReal ((2 * A) ^ q.toReal * q.toReal) * ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹) := by - unfold sel - dsimp only + dsimp only [sel] ring_nf _ = (if q₁ < ⊤ then 1 else 0) * (↑C₀ ^ ((1 - t) * q.toReal) * ↑C₁ ^ (t * q.toReal) * eLpNorm f p μ ^ q.toReal * @@ -3870,7 +3839,7 @@ lemma exists_hasStrongType_real_interpolation_aux {p₀ p₁ q₀ q₁ p q : ℝ apply exists_hasStrongType_real_interpolation_aux₀ (hp := hp) (hq := hq) <;> try assumption · let spf := spf_ch ht hq₀q₁ hp₀.1 hq₀ hp₁.1 hq₁ hp₀p₁.ne hC₀ hC₁ ⟨hF, hf.2⟩ apply combine_estimates₁ <;> try assumption - on_goal 1 => unfold_let spf + on_goal 1 => unfold spf rfl -- TODO: the below lemmas were split because otherwise the lean server would crash @@ -4028,7 +3997,7 @@ lemma exists_hasStrongType_real_interpolation_aux₂ {f : α → E₁} · have p₀pos : p₀ > 0 := hp₀.1 have p₁pos : p₁ > 0 := hp₁.1 have q₀ne_top : q₀ ≠ ⊤ := hq₀q₁.ne_top - unfold_let M at ht + unfold M at ht rw [d_eq_top_of_eq] at ht <;> try assumption have : ENNReal.ofReal (C₁ * eLpNorm f p μ).toReal = C₁ * eLpNorm f p μ := by refine ofReal_toReal_eq_iff.mpr ?_ diff --git a/Carleson/ToMathlib/ENorm.lean b/Carleson/ToMathlib/ENorm.lean index 4a751906..fa9a936e 100644 --- a/Carleson/ToMathlib/ENorm.lean +++ b/Carleson/ToMathlib/ENorm.lean @@ -140,13 +140,6 @@ def HasBoundedStrongType {E E' α α' : Type*} [NormedAddCommGroup E] [NormedAdd ∀ f : α → E, Memℒp f p μ → eLpNorm f ∞ μ < ∞ → μ (support f) < ∞ → AEStronglyMeasurable (T f) ν ∧ eLpNorm (T f) p' ν ≤ c * eLpNorm f p μ -/- Mathlib PR: https://github.com/leanprover-community/mathlib4/pull/18704. -/ -lemma _root_.ENNReal.inv_div {a b : ℝ≥0∞} (h1 : b ≠ ∞ ∨ a ≠ ∞) (h2 : b ≠ 0 ∨ a ≠ 0) : - (a / b)⁻¹ = b / a := by - rw [← ENNReal.inv_ne_zero] at h1 - rw [← ENNReal.inv_ne_top] at h2 - rw [ENNReal.div_eq_inv_mul, ENNReal.div_eq_inv_mul, ENNReal.mul_inv h1 h2, mul_comm, inv_inv] - /-- If a function `f : α → ENNReal` is `MemWℒp`, then its norm is almost everywhere finite.-/ theorem MemWℒp.ae_ne_top [TopologicalSpace E] [ENorm E] {f : α → E} {p : ℝ≥0∞} {μ : Measure α} (hf : MemWℒp f p μ) : ∀ᵐ x ∂μ, ‖f x‖ₑ ≠ ∞ := by @@ -346,18 +339,18 @@ theorem _root_.Set.Countable.measure_biUnion_le_lintegral [OpensMeasurableSpace hB (Subtype.coe_prop i) (Subtype.coe_prop j) (Subtype.coe_ne_coe.mpr hij) calc l * μ (⋃ i ∈ 𝓑, ball (c i) (r i)) ≤ l * μ (⋃ i ∈ B, ball (c i) (2 ^ 2 * r i)) := by - refine l.mul_left_mono (μ.mono fun x hx ↦ ?_) + refine mul_left_mono (μ.mono fun x hx ↦ ?_) simp only [mem_iUnion, mem_ball, exists_prop] at hx rcases hx with ⟨i, i𝓑, hi⟩ obtain ⟨b, bB, hb⟩ := h2B i i𝓑 refine mem_iUnion₂.mpr ⟨b, bB, hb <| mem_ball.mpr hi⟩ _ ≤ l * ∑' i : B, μ (ball (c i) (2 ^ 2 * r i)) := - l.mul_left_mono <| measure_biUnion_le μ (h𝓑.mono hB𝓑) fun i ↦ ball (c i) (2 ^ 2 * r i) + mul_left_mono <| measure_biUnion_le μ (h𝓑.mono hB𝓑) fun i ↦ ball (c i) (2 ^ 2 * r i) _ ≤ l * ∑' i : B, A ^ 2 * μ (ball (c i) (r i)) := by - refine l.mul_left_mono <| ENNReal.tsum_le_tsum (fun i ↦ ?_) + refine mul_left_mono <| ENNReal.tsum_le_tsum (fun i ↦ ?_) rw [sq, sq, mul_assoc, mul_assoc] apply (Measure.IsDoubling.measure_ball_two_le_same (c i) (2 * r i)).trans - exact ENNReal.mul_left_mono (Measure.IsDoubling.measure_ball_two_le_same (c i) (r i)) + exact mul_left_mono (Measure.IsDoubling.measure_ball_two_le_same (c i) (r i)) _ = A ^ 2 * ∑' i : B, l * μ (ball (c i) (r i)) := by rw [ENNReal.tsum_mul_left, ENNReal.tsum_mul_left, ← mul_assoc, ← mul_assoc, mul_comm l] _ ≤ A ^ 2 * ∑' i : B, ∫⁻ x in ball (c i) (r i), u x ∂μ := by diff --git a/Carleson/ToMathlib/Misc.lean b/Carleson/ToMathlib/Misc.lean index d52e3f7a..cf8d79f0 100644 --- a/Carleson/ToMathlib/Misc.lean +++ b/Carleson/ToMathlib/Misc.lean @@ -16,49 +16,6 @@ import Carleson.ToMathlib.MeasureReal open Function Set open scoped ENNReal -section Metric - -attribute [gcongr] Metric.ball_subset_ball - - -lemma Metric.dense_iff_iUnion_ball {X : Type*} [PseudoMetricSpace X] (s : Set X) : - Dense s ↔ ∀ r > 0, ⋃ c ∈ s, ball c r = univ := by - simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop, mem_ball, Dense, Metric.mem_closure_iff, - forall_comm (α := X)] - -theorem PseudoMetricSpace.dist_eq_of_dist_zero {X : Type*} [PseudoMetricSpace X] (x : X) {y y' : X} - (hyy' : dist y y' = 0) : dist x y = dist x y' := - dist_comm y x ▸ dist_comm y' x ▸ sub_eq_zero.1 (abs_nonpos_iff.1 (hyy' ▸ abs_dist_sub_le y y' x)) - -end Metric - -section Order - -lemma IsTop.isMax_iff {α} [PartialOrder α] {i j : α} (h : IsTop i) : IsMax j ↔ j = i := by - simp_rw [le_antisymm_iff, h j, true_and] - refine ⟨(· (h j)), swap (fun _ ↦ h · |>.trans ·)⟩ - -end Order - -section Int - -theorem Int.floor_le_iff (c : ℝ) (z : ℤ) : ⌊c⌋ ≤ z ↔ c < z + 1 := by - rw_mod_cast [← Int.floor_le_sub_one_iff, add_sub_cancel_right] - -theorem Int.Icc_of_eq_sub_1 {a b : ℤ} (h : a = b - 1) : Finset.Icc a b = {a, b} := by - refine le_antisymm (fun t ht ↦ ?_) (fun t ht ↦ ?_) - · rw [h, Finset.mem_Icc] at ht - by_cases hta : t = b - 1 - · rw [hta, ← h]; exact Finset.mem_insert_self a {b} - · suffices b = t from this ▸ Finset.mem_insert.2 (Or.inr (Finset.mem_singleton.2 rfl)) - exact le_antisymm (sub_add_cancel b 1 ▸ (ne_eq t (b - 1) ▸ hta).symm.lt_of_le ht.1) ht.2 - · have hab : a ≤ b := h ▸ sub_le_self b one_pos.le - rcases Finset.mem_insert.1 ht with rfl | hb - · exact Finset.mem_Icc.2 ⟨le_refl t, hab⟩ - · rw [Finset.mem_singleton.1 hb]; exact Finset.mem_Icc.2 ⟨hab, le_refl b⟩ - -end Int - section ENNReal lemma tsum_one_eq' {α : Type*} (s : Set α) : ∑' (_:s), (1 : ℝ≥0∞) = s.encard := by @@ -96,12 +53,15 @@ lemma tsum_one_eq' {α : Type*} (s : Set α) : ∑' (_:s), (1 : ℝ≥0∞) = s. rw [Set.encard_eq_top_iff.mpr hfin] simp only [ENat.toENNReal_top] +#find_home! tsum_one_eq' lemma ENNReal.tsum_const_eq' {α : Type*} (s : Set α) (c : ℝ≥0∞) : ∑' (_:s), (c : ℝ≥0∞) = s.encard * c := by nth_rw 1 [← one_mul c] rw [ENNReal.tsum_mul_right,tsum_one_eq'] +#find_home! ENNReal.tsum_const_eq' + /-! ## `ENNReal` manipulation lemmas -/ lemma ENNReal.sum_geometric_two_pow_toNNReal {k : ℕ} (hk : k > 0) : diff --git a/lake-manifest.json b/lake-manifest.json index f7c94c0f..143f7f19 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18", + "rev": "a822446d61ad7e7f5e843365c7041c326553050a", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785", + "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5f934891e11d70a1b86e302fdf9cecfc21e8de46", + "rev": "de91b59101763419997026c35a41432ac8691f15", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,17 +35,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "23268f52d3505955de3c26a42032702c25cfcbf8", + "rev": "1383e72b40dd62a566896a6e348ffe868801b172", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.44", + "inputRev": "v0.0.46", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", + "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb", + "rev": "119b022b3ea88ec810a677888528e50f8144a26e", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7bedaed1ef024add1e171cc17706b012a9a37802", + "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d212dd74414e997653cd3484921f4159c955ccca", + "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "d7317655e2826dc1f1de9a0c138db2775c4bb841", + "rev": "840e02ce2768e06de7ced0a624444746590e9d99", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "stable", + "inputRev": null, "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/PatrickMassot/checkdecls.git", diff --git a/lakefile.toml b/lakefile.toml index 8bdf458a..c7dbe481 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -15,7 +15,6 @@ linter.flexible = true [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" -rev = "stable" [[require]] name = "checkdecls" diff --git a/lean-toolchain b/lean-toolchain index 4f86f953..57a4710c 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.13.0 +leanprover/lean4:v4.14.0-rc2