From 6d3cbe78cc020c26f7a41cd37bef9d472d3522f0 Mon Sep 17 00:00:00 2001 From: Jeremy Tan Jie Rui Date: Mon, 9 Sep 2024 13:34:04 +0800 Subject: [PATCH] Update mathlib to 4.12.0-rc1 (#114) @fpvandoorn I can now report that the `Nat.reducePow` bug that was causing PANICs in builds of this repo has been fixed. --- Carleson/AntichainOperator.lean | 5 +--- Carleson/Classical/Approximation.lean | 2 +- Carleson/Classical/CarlesonOnTheRealLine.lean | 9 ++++--- Carleson/Classical/CarlesonOperatorReal.lean | 6 ++--- Carleson/Classical/ClassicalCarleson.lean | 2 +- .../Classical/ControlApproximationEffect.lean | 9 ++++--- Carleson/Classical/Helper.lean | 2 +- Carleson/Classical/HilbertKernel.lean | 2 +- Carleson/Classical/VanDerCorput.lean | 4 +-- Carleson/Defs.lean | 3 --- Carleson/Discrete/Defs.lean | 3 --- Carleson/Discrete/ExceptionalSet.lean | 9 +++---- Carleson/Discrete/Forests.lean | 3 --- Carleson/FinitaryCarleson.lean | 3 --- Carleson/Forest.lean | 3 --- Carleson/GridStructure.lean | 7 ++--- Carleson/HardyLittlewood.lean | 8 +++--- Carleson/Psi.lean | 27 +++++++++---------- Carleson/RealInterpolation.lean | 4 +-- Carleson/TileExistence.lean | 21 +++++++-------- Carleson/TileStructure.lean | 3 --- Carleson/ToMathlib/Height.lean | 17 ++---------- Carleson/ToMathlib/MeasureReal.lean | 4 +-- Carleson/WeakType.lean | 4 +-- lake-manifest.json | 16 +++++------ lean-toolchain | 2 +- 26 files changed, 68 insertions(+), 110 deletions(-) diff --git a/Carleson/AntichainOperator.lean b/Carleson/AntichainOperator.lean index 82f9c2c3..da5dcf04 100644 --- a/Carleson/AntichainOperator.lean +++ b/Carleson/AntichainOperator.lean @@ -2,9 +2,6 @@ import Carleson.TileStructure import Carleson.HardyLittlewood import Carleson.Psi --- https://github.com/leanprover/lean4/issues/4947 -attribute [-simp] Nat.reducePow - open scoped ShortVariables variable {X : Type*} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q D κ S o] @@ -260,7 +257,7 @@ lemma Dens2Antichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤·) ( rw [one_le_div (add_pos_iff.mpr (Or.inr zero_lt_one)), two_mul, add_le_add_iff_left] exact le_of_lt (q_mem_Ioc X).1 have hqq' : q' ≤ nnq := by -- Better proof? - rw [add_comm, div_le_iff (add_pos (zero_lt_one) hq0), mul_comm, mul_le_mul_iff_of_pos_left hq0, + rw [add_comm, div_le_iff₀ (add_pos (zero_lt_one) hq0), mul_comm, mul_le_mul_iff_of_pos_left hq0, ← one_add_one_eq_two, add_le_add_iff_left] exact (nnq_mem_Ioc X).1.le have hq'_inv : (q' - 1)⁻¹ ≤ 3 * (nnq - 1)⁻¹ := by diff --git a/Carleson/Classical/Approximation.lean b/Carleson/Classical/Approximation.lean index 6ddbbab7..8dffe733 100644 --- a/Carleson/Classical/Approximation.lean +++ b/Carleson/Classical/Approximation.lean @@ -72,7 +72,7 @@ lemma fourierCoeffOn_bound {f : ℝ → ℂ} (f_continuous : Continuous f) : ∃ fourier_coe_apply', Complex.ofReal_mul, Complex.ofReal_ofNat, smul_eq_mul, Complex.real_smul, Complex.ofReal_inv, map_mul, map_inv₀, Complex.abs_ofReal, Complex.abs_ofNat] field_simp - rw [abs_of_nonneg Real.pi_pos.le, mul_comm Real.pi, div_le_iff Real.two_pi_pos, ←Complex.norm_eq_abs] + rw [abs_of_nonneg Real.pi_pos.le, mul_comm Real.pi, div_le_iff₀ Real.two_pi_pos, ←Complex.norm_eq_abs] calc ‖∫ (x : ℝ) in (0 : ℝ)..(2 * Real.pi), (starRingEnd ℂ) (Complex.exp (2 * Real.pi * Complex.I * n * x / (2 * Real.pi))) * f x‖ _ = ‖∫ (x : ℝ) in (0 : ℝ)..(2 * Real.pi), (starRingEnd ℂ) (Complex.exp (Complex.I * n * x)) * f x‖ := by congr with x diff --git a/Carleson/Classical/CarlesonOnTheRealLine.lean b/Carleson/Classical/CarlesonOnTheRealLine.lean index d8086189..69a277db 100644 --- a/Carleson/Classical/CarlesonOnTheRealLine.lean +++ b/Carleson/Classical/CarlesonOnTheRealLine.lean @@ -48,6 +48,7 @@ def integer_linear (n : ℤ) : C(ℝ, ℝ) := ⟨fun (x : ℝ) ↦ n * x, by fun local notation "θ" => integer_linear +set_option quotPrecheck false in local notation "Θ" => {(θ n) | n : ℤ} @@ -454,7 +455,7 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where by_cases hxy : x = y · rw [hxy] simp - rw [dist_eq_norm, ← div_le_iff (dist_pos.mpr hxy), Ldef, NNReal.coe_mk] + rw [dist_eq_norm, ← div_le_iff₀ (dist_pos.mpr hxy), Ldef, NNReal.coe_mk] apply le_ciSup_of_le _ x apply le_ciSup_of_le _ y apply le_ciSup_of_le _ hxy @@ -464,7 +465,7 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where simp only [ne_eq, Set.mem_range, exists_prop, and_imp, forall_apply_eq_imp_iff, Set.mem_setOf_eq] intro h - rw [div_le_iff (dist_pos.mpr h), dist_eq_norm] + rw [div_le_iff₀ (dist_pos.mpr h), dist_eq_norm] exact LipschitzWith.norm_sub_le hK _ _ · use K rw [upperBounds] @@ -473,7 +474,7 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where intro y apply Real.iSup_le _ NNReal.zero_le_coe intro h - rw [div_le_iff (dist_pos.mpr h), dist_eq_norm] + rw [div_le_iff₀ (dist_pos.mpr h), dist_eq_norm] exact LipschitzWith.norm_sub_le hK _ _ · use K rw [upperBounds] @@ -484,7 +485,7 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where intro y apply Real.iSup_le _ NNReal.zero_le_coe intro h - rw [div_le_iff (dist_pos.mpr h), dist_eq_norm] + rw [div_le_iff₀ (dist_pos.mpr h), dist_eq_norm] apply LipschitzWith.norm_sub_le hK · --prove main property of B intro y hy diff --git a/Carleson/Classical/CarlesonOperatorReal.lean b/Carleson/Classical/CarlesonOperatorReal.lean index 7a6f3264..caa53018 100644 --- a/Carleson/Classical/CarlesonOperatorReal.lean +++ b/Carleson/Classical/CarlesonOperatorReal.lean @@ -94,7 +94,7 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab use S constructor · intro s hs - apply Filter.eventually_of_forall + apply Filter.Eventually.of_forall intro y rw [bound_def, Fdef, norm_indicator_eq_indicator_norm] simp only @@ -138,7 +138,7 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab · --interesting part rw [MeasureTheory.ae_restrict_iff' annulus_measurableSet] simp_rw [norm_norm] - apply Filter.eventually_of_forall + apply Filter.Eventually.of_forall apply F_bound_on_set · have contOn1 : ∀ (y : ℝ), ContinuousOn (fun s ↦ F x s y) (Set.Iio (dist x y)) := by intro y @@ -202,7 +202,7 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab · right; linarith rw [MeasureTheory.ae_iff] exact MeasureTheory.measure_mono_null subset_finite (Finset.measure_zero _ _) - · exact Filter.eventually_of_forall fun r ↦ ((Measurable.of_uncurry_left + · exact Filter.Eventually.of_forall fun r ↦ ((Measurable.of_uncurry_left (measurable_mul_kernel f_measurable)).indicator annulus_measurableSet).aestronglyMeasurable rw [this] apply measurable_biSup _ diff --git a/Carleson/Classical/ClassicalCarleson.lean b/Carleson/Classical/ClassicalCarleson.lean index a9c3fe0b..025efd63 100644 --- a/Carleson/Classical/ClassicalCarleson.lean +++ b/Carleson/Classical/ClassicalCarleson.lean @@ -63,7 +63,7 @@ theorem classical_carleson {f : ℝ → ℂ} gcongr rw [ε'def, div_div] apply div_le_div_of_nonneg_left εpos.le (by norm_num) - rw [← div_le_iff' (by norm_num)] + rw [← div_le_iff₀' (by norm_num)] exact le_trans' (lt_C_control_approximation_effect εpos).le (by linarith [Real.two_le_pi]) _ ≤ ε := by linarith diff --git a/Carleson/Classical/ControlApproximationEffect.lean b/Carleson/Classical/ControlApproximationEffect.lean index 2fa30a50..552c6a65 100644 --- a/Carleson/Classical/ControlApproximationEffect.lean +++ b/Carleson/Classical/ControlApproximationEffect.lean @@ -127,7 +127,8 @@ lemma Dirichlet_Hilbert_diff {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc (-Real.pi) _ = 2 * (|x| / ‖1 - exp (I * x)‖) := by ring _ ≤ 2 * (Real.pi / 2) := by gcongr 2 * ?_ - rw [div_le_iff' (by rwa [norm_pos_iff]), ←div_le_iff (by linarith [Real.pi_pos]), div_div_eq_mul_div, mul_div_assoc, mul_comm] + rw [div_le_iff₀' (by rwa [norm_pos_iff]), ← div_le_iff₀ (by linarith [Real.pi_pos]), + div_div_eq_mul_div, mul_div_assoc, mul_comm] apply lower_secant_bound' (by rfl) have : |x| ≤ Real.pi := by rwa [abs_le] @@ -343,14 +344,14 @@ lemma le_CarlesonOperatorReal {g : ℝ → ℂ} (hg : IntervalIntegrable g Measu · conv => pattern ((g _) * _); rw [mul_comm] apply MeasureTheory.Integrable.bdd_mul' integrable₁ measurable₁.aestronglyMeasurable · rw [MeasureTheory.ae_restrict_iff' annulus_measurableSet] - apply eventually_of_forall + apply Eventually.of_forall exact fun _ hy ↦ boundedness₁ hy.1.le · conv => pattern ((g _) * _); rw [mul_comm] apply MeasureTheory.Integrable.bdd_mul' integrable₁ · apply Measurable.aestronglyMeasurable exact continuous_star.measurable.comp measurable₁ · rw [MeasureTheory.ae_restrict_iff' annulus_measurableSet] - apply eventually_of_forall + apply Eventually.of_forall intro y hy rw [RCLike.norm_conj] exact boundedness₁ hy.1.le @@ -636,7 +637,7 @@ lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ : _ ≤ 2 * (δ * C10_0_1 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹ / (Real.pi * (ε' - Real.pi * δ))) ^ (2 : ℝ) := by rw [Real.rpow_mul MeasureTheory.measureReal_nonneg] gcongr - rw [Real.rpow_add' MeasureTheory.measureReal_nonneg (by norm_num), Real.rpow_one, le_div_iff' ε'_δ_expression_pos, ← mul_assoc] + rw [Real.rpow_add' MeasureTheory.measureReal_nonneg (by norm_num), Real.rpow_one, le_div_iff₀' ε'_δ_expression_pos, ← mul_assoc] apply mul_le_of_nonneg_of_le_div δ_mul_const_pos.le apply Real.rpow_nonneg MeasureTheory.measureReal_nonneg rw[Real.rpow_neg MeasureTheory.measureReal_nonneg, div_inv_eq_mul] diff --git a/Carleson/Classical/Helper.lean b/Carleson/Classical/Helper.lean index aa70d7af..ea00ce96 100644 --- a/Carleson/Classical/Helper.lean +++ b/Carleson/Classical/Helper.lean @@ -19,7 +19,7 @@ lemma intervalIntegrable_of_bdd {a b : ℝ} {δ : ℝ} {g : ℝ → ℂ} (measur · exact intervalIntegrable_const · exact measurable_g.aestronglyMeasurable · rw [Filter.EventuallyLE, ae_restrict_iff_subtype measurableSet_uIoc] - apply Filter.eventually_of_forall + apply Filter.Eventually.of_forall rw [Subtype.forall] exact fun x _ ↦ bddg x diff --git a/Carleson/Classical/HilbertKernel.lean b/Carleson/Classical/HilbertKernel.lean index 5770beff..6be76458 100644 --- a/Carleson/Classical/HilbertKernel.lean +++ b/Carleson/Classical/HilbertKernel.lean @@ -252,7 +252,7 @@ lemma Hilbert_kernel_regularity {x y y' : ℝ} : /- Beginning of the main proof -/ have y2ley' : y / 2 ≤ y' := by - rw [div_le_iff two_pos] + rw [div_le_iff₀ two_pos] calc y _ = 2 * (y - y') - y + 2 * y' := by ring _ ≤ 2 * |y - y'| - y + 2 * y' := by gcongr; exact le_abs_self _ diff --git a/Carleson/Classical/VanDerCorput.lean b/Carleson/Classical/VanDerCorput.lean index dcc20cc5..76cf0a5a 100644 --- a/Carleson/Classical/VanDerCorput.lean +++ b/Carleson/Classical/VanDerCorput.lean @@ -36,7 +36,7 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B case to the complex conjugate.-/ push_neg at n_pos calc ‖∫ (x : ℝ) in a..b, cexp (I * ↑n * ↑x) * ϕ x‖ - _ = ‖(starRingEnd ℂ) (∫ (x : ℝ) in a..b, cexp (I * ↑n * ↑x) * ϕ x)‖ := Eq.symm RCLike.norm_conj + _ = ‖(starRingEnd ℂ) (∫ (x : ℝ) in a..b, cexp (I * ↑n * ↑x) * ϕ x)‖ := Eq.symm (RCLike.norm_conj _) _ = ‖∫ (x : ℝ) in a..b, cexp (I * ↑(-n) * ↑x) * ((starRingEnd ℂ) ∘ ϕ) x‖ := by rw [intervalIntegral.integral_of_le (by linarith), ← integral_conj, ← intervalIntegral.integral_of_le (by linarith)] congr @@ -214,7 +214,7 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B linarith [Real.two_le_pi] _ ≤ Real.pi * (n * (b - a) + n * (b - a)) := by gcongr - rwa [← div_le_iff' (Int.cast_pos.mpr n_pos)] + rwa [← div_le_iff₀' (Int.cast_pos.mpr n_pos)] _ = (b - a) * (2 * Real.pi) * n := by ring exact add_pos zero_lt_one (mul_pos (Int.cast_pos.mpr n_pos) (gt_of_ge_of_gt h pi_div_n_pos)) _ = 2 * Real.pi * (b - a) * (B + K * (b - a) / 2) * (1 + |n| * (b - a))⁻¹ := by diff --git a/Carleson/Defs.lean b/Carleson/Defs.lean index 0524f8fd..d8c076fb 100644 --- a/Carleson/Defs.lean +++ b/Carleson/Defs.lean @@ -1,9 +1,6 @@ import Carleson.DoublingMeasure import Carleson.WeakType --- https://github.com/leanprover/lean4/issues/4947 -attribute [-simp] Nat.reducePow - open MeasureTheory Measure NNReal Metric Complex Set TopologicalSpace Bornology Function open scoped ENNReal noncomputable section diff --git a/Carleson/Discrete/Defs.lean b/Carleson/Discrete/Defs.lean index ebf633e4..d00c6115 100644 --- a/Carleson/Discrete/Defs.lean +++ b/Carleson/Discrete/Defs.lean @@ -1,9 +1,6 @@ import Carleson.Forest import Carleson.MinLayerTiles --- https://github.com/leanprover/lean4/issues/4947 -attribute [-simp] Nat.reducePow - open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators Bornology open scoped ENNReal open Classical -- We use quite some `Finset.filter` diff --git a/Carleson/Discrete/ExceptionalSet.lean b/Carleson/Discrete/ExceptionalSet.lean index 783e7619..99795f00 100644 --- a/Carleson/Discrete/ExceptionalSet.lean +++ b/Carleson/Discrete/ExceptionalSet.lean @@ -1,9 +1,6 @@ import Carleson.Discrete.Defs import Carleson.HardyLittlewood --- https://github.com/leanprover/lean4/issues/4947 -attribute [-simp] Nat.reducePow - open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators Bornology open scoped ENNReal open Classical -- We use quite some `Finset.filter` @@ -74,7 +71,7 @@ lemma first_exception' : volume (G₁ : Set X) ≤ 2 ^ (- 5 : ℤ) * volume G := exact mul_pos_iff.2 ⟨ENNReal.pow_pos two_pos _, measure_pos_of_superset subset_rfl hF⟩ have K_ne_top : K ≠ ⊤ := by simp only [K] - refine ne_of_lt (div_lt_top (ne_of_lt (mul_lt_top (pow_ne_top two_ne_top) ?_)) hG) + refine (div_lt_top (mul_ne_top (pow_ne_top two_ne_top) ?_) hG).ne exact (measure_mono (ProofData.F_subset)).trans_lt measure_ball_lt_top |>.ne -- Define function `r : 𝔓 X → ℝ`, with garbage value `0` for `p ∉ highDensityTiles` have : ∀ p ∈ highDensityTiles, ∃ r ≥ 4 * (D : ℝ) ^ 𝔰 p, @@ -206,8 +203,8 @@ lemma john_nirenberg_aux1 {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n)) at mx simp_rw [mem_setOf_eq, and_assoc] at mx have mid0 : stackSize { p' ∈ 𝔐 k n | ¬𝓘 p' ≤ L ∧ Disjoint (𝓘 p' : Set X) L} x = 0 := by - simp_rw [stackSize, Finset.sum_eq_zero_iff, indicator_apply_eq_zero, imp_false, - Finset.mem_filter, Finset.mem_univ, true_and] + simp_rw [stackSize, Finset.sum_eq_zero_iff, indicator_apply_eq_zero, + show ¬(1 : X → ℕ) x = 0 by simp, imp_false, Finset.mem_filter, Finset.mem_univ, true_and] rintro y ⟨-, -, dj2⟩ exact disjoint_right.mp dj2 mx₂ rw [mid0, zero_add] at mx diff --git a/Carleson/Discrete/Forests.lean b/Carleson/Discrete/Forests.lean index 7e46b409..cdd521b2 100644 --- a/Carleson/Discrete/Forests.lean +++ b/Carleson/Discrete/Forests.lean @@ -1,8 +1,5 @@ import Carleson.Discrete.ExceptionalSet --- https://github.com/leanprover/lean4/issues/4947 -attribute [-simp] Nat.reducePow - open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators Bornology open scoped ENNReal open Classical -- We use quite some `Finset.filter` diff --git a/Carleson/FinitaryCarleson.lean b/Carleson/FinitaryCarleson.lean index f81d75e6..b75db773 100644 --- a/Carleson/FinitaryCarleson.lean +++ b/Carleson/FinitaryCarleson.lean @@ -1,9 +1,6 @@ import Carleson.Discrete.Forests import Carleson.TileExistence --- https://github.com/leanprover/lean4/issues/4947 -attribute [-simp] Nat.reducePow - open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators Bornology Classical open scoped ENNReal noncomputable section diff --git a/Carleson/Forest.lean b/Carleson/Forest.lean index acdf2374..79a7df3c 100644 --- a/Carleson/Forest.lean +++ b/Carleson/Forest.lean @@ -1,8 +1,5 @@ import Carleson.TileStructure --- https://github.com/leanprover/lean4/issues/4947 -attribute [-simp] Nat.reducePow - open Set MeasureTheory Metric Function Complex Bornology Classical open scoped NNReal ENNReal ComplexConjugate noncomputable section diff --git a/Carleson/GridStructure.lean b/Carleson/GridStructure.lean index a9cf937a..502d9b75 100644 --- a/Carleson/GridStructure.lean +++ b/Carleson/GridStructure.lean @@ -1,8 +1,5 @@ import Carleson.Defs --- https://github.com/leanprover/lean4/issues/4947 -attribute [-simp] Nat.reducePow - open Set MeasureTheory Metric Function Complex Bornology open scoped NNReal ENNReal ComplexConjugate noncomputable section @@ -63,7 +60,7 @@ variable {i j : Grid X} instance : Inhabited (Grid X) := ⟨topCube⟩ instance : Fintype (Grid X) := GridStructure.fintype_Grid instance : Coe (Grid X) (Set X) := ⟨GridStructure.coeGrid⟩ -instance : Membership X (Grid X) := ⟨fun x i ↦ x ∈ (i : Set X)⟩ +instance : Membership X (Grid X) := ⟨fun i x ↦ x ∈ (i : Set X)⟩ instance : PartialOrder (Grid X) := PartialOrder.lift _ GridStructure.inj /- These should probably not/only rarely be used. I comment them out for now, so that we don't accidentally use it. We can put it back if useful after all. -/ @@ -306,7 +303,7 @@ lemma dist_strictMono {I J : Grid X} (hpq : I < J) {f g : Θ X} : _ ≤ dist_{c I, 4 * D ^ s I} f g := cdist_mono (ball_subset_ball (by simp_rw [div_eq_inv_mul, defaultD]; gcongr; norm_num)) _ ≤ 2 ^ (-100 * (a : ℝ)) * dist_{c I, 4 * D ^ (s I + 1)} f g := by - rw [← div_le_iff' (by positivity), neg_mul, Real.rpow_neg zero_le_two, div_inv_eq_mul, mul_comm] + rw [← div_le_iff₀' (by positivity), neg_mul, Real.rpow_neg zero_le_two, div_inv_eq_mul, mul_comm] convert le_cdist_iterate (x := c I) (r := 4 * D ^ s I) (by positivity) f g (100 * a) using 1 · norm_cast · apply dist_congr rfl diff --git a/Carleson/HardyLittlewood.lean b/Carleson/HardyLittlewood.lean index cda04c05..9f5f800b 100644 --- a/Carleson/HardyLittlewood.lean +++ b/Carleson/HardyLittlewood.lean @@ -60,8 +60,8 @@ private lemma P'_of_P [BorelSpace X] [ProperSpace X] [IsFiniteMeasureOnCompacts (coe_nnnorm_ae_le_eLpNormEssSup u μ).mono (by tauto) apply lt_of_le_of_lt (MeasureTheory.setLIntegral_mono_ae' measurableSet_ball hfg) rw [MeasureTheory.setLIntegral_const (ball c r) (eLpNormEssSup u μ)] - refine ENNReal.mul_lt_top ?_ (measure_ball_ne_top c r) - exact eLpNorm_exponent_top (f := u) ▸ hu.eLpNorm_lt_top |>.ne + refine ENNReal.mul_lt_top ?_ measure_ball_lt_top + exact eLpNorm_exponent_top (f := u) ▸ hu.eLpNorm_lt_top · have := hu.eLpNorm_lt_top simp [eLpNorm, one_ne_zero, reduceIte, ENNReal.one_ne_top, eLpNorm', ENNReal.one_toReal, ENNReal.rpow_one, ne_eq, not_false_eq_true, div_self] at this @@ -80,7 +80,7 @@ private lemma P'.add [MeasurableSpace E] [BorelSpace E] private lemma P'.smul [NormedSpace ℝ E] {f : X → E} (hf : P' μ f) (s : ℝ) : P' μ (s • f) := by refine ⟨AEStronglyMeasurable.const_smul hf.1 s, fun c r ↦ ?_⟩ simp_rw [Pi.smul_apply, nnnorm_smul, ENNReal.coe_mul, lintegral_const_mul' _ _ ENNReal.coe_ne_top] - exact ENNReal.mul_lt_top ENNReal.coe_ne_top (hf.2 c r).ne + exact ENNReal.mul_lt_top ENNReal.coe_lt_top (hf.2 c r) -- The average that appears in the definition of `MB` variable (μ c r) in @@ -165,7 +165,7 @@ protected theorem HasStrongType.MB_top [BorelSpace X] (h𝓑 : 𝓑.Countable) : intro f _ use AEStronglyMeasurable.maximalFunction_toReal h𝓑 simp only [ENNReal.coe_one, one_mul, eLpNorm_exponent_top] - refine essSup_le_of_ae_le _ (eventually_of_forall fun x ↦ ?_) + refine essSup_le_of_ae_le _ (Eventually.of_forall fun x ↦ ?_) simp_rw [ENNReal.nnorm_toReal] refine ENNReal.coe_toNNReal_le_self |>.trans ?_ apply MB_le_eLpNormEssSup diff --git a/Carleson/Psi.lean b/Carleson/Psi.lean index 077fe079..652d4460 100644 --- a/Carleson/Psi.lean +++ b/Carleson/Psi.lean @@ -1,8 +1,5 @@ import Carleson.Defs --- https://github.com/leanprover/lean4/issues/4947 -attribute [-simp] Nat.reducePow - open MeasureTheory Measure NNReal Metric Set TopologicalSpace Function DoublingMeasure open scoped ENNReal noncomputable section @@ -49,15 +46,15 @@ lemma ψ_formula₀ {x : ℝ} (hx : x ≤ 1 / (4 * D : ℝ)) : ψ D x = 0 := by by_cases hD : D = 0 · simp [ψ, hD] · exact max_eq_left <| (min_le_right 1 _).trans <| (min_le_left _ _).trans <| - tsub_nonpos.2 <| (_root_.le_div_iff' (mul_pos four_pos + tsub_nonpos.2 <| (le_div_iff₀' (mul_pos four_pos (by exact_mod_cast Nat.zero_lt_of_ne_zero hD))).1 hx include hD in lemma ψ_formula₁ {x : ℝ} (hx : 1 / (4 * D) ≤ x ∧ x ≤ 1 / (2 * D)) : ψ D x = 4 * D * x - 1 := by have : x ≥ 0 := le_trans (one_div_nonneg.2 (le_of_lt <| fourD0 hD)) hx.1 - have hx1 := (div_le_iff' (fourD0 hD)).1 hx.1 - have hx2 := (le_div_iff' (twoD0 hD)).1 hx.2 + have hx1 := (div_le_iff₀' (fourD0 hD)).1 hx.1 + have hx2 := (le_div_iff₀' (twoD0 hD)).1 hx.2 have ineq₀ : 4 * D * x - 1 ≤ 2 - 4 * x := by suffices (2 * D + 2 * D + 4) * x ≤ 3 by linarith exact le_trans (by gcongr; linarith [D2 hD]) (by linarith: (2 * D + 2 * D + 2 * D) * x ≤ 3) @@ -69,7 +66,7 @@ include hD in lemma ψ_formula₂ {x : ℝ} (hx : 1 / (2 * D) ≤ x ∧ x ≤ 1 / 4) : ψ D x = 1 := by unfold ψ suffices min 1 (min (4 * D * x - 1) (2 - 4 * x)) = 1 from this.symm ▸ max_eq_right_of_lt one_pos - have := (div_le_iff' (twoD0 hD)).1 hx.1 + have := (div_le_iff₀' (twoD0 hD)).1 hx.1 exact min_eq_left (le_min (by linarith) (by linarith)) include hD in @@ -161,7 +158,7 @@ show that `nonzeroS D x` has either 1 or 2 elements. The next two lemmas prove ` include hD private lemma le_div_ceil_mul (hx : 0 < x) : 1 / (4 * D) ≤ D ^ (-⌈logb D (4 * x)⌉) * x := by - rw [← div_le_iff hx, div_div, ← rpow_logb (D0 hD) (ne_of_gt hD) (cDx0 hD four_pos hx), + rw [← div_le_iff₀ hx, div_div, ← rpow_logb (D0 hD) (ne_of_gt hD) (cDx0 hD four_pos hx), ← inv_eq_one_div, (by norm_cast : (D : ℝ) ^ (-⌈logb D (4 * x)⌉) = D ^ (-⌈logb D (4 * x)⌉ : ℝ)), ← rpow_neg (D0 hD).le, rpow_le_rpow_left_iff hD, neg_le_neg_iff] apply le_of_le_of_eq <| calc @@ -240,8 +237,8 @@ private lemma sum_ψ₂ (hx : 0 < x) rw [zpow_sub₀ (ne_of_gt (D0 hD)), zpow_neg, zpow_one, div_eq_mul_inv] rw [neg_sub, sub_eq_add_neg, zpow_add₀ (ne_of_gt (D0 hD)), zpow_one, mul_assoc] constructor - · rw [← div_le_iff' (D0 hD), div_div]; exact hs₀.1 - · rw [← le_div_iff' (D0 hD), div_div]; exact hs₀.2 + · rw [← div_le_iff₀' (D0 hD), div_div]; exact hs₀.1 + · rw [← le_div_iff₀' (D0 hD), div_div]; exact hs₀.2 -- See `finsum_ψ` for the version that doesn't explicitly restrict to the support. lemma sum_ψ (hx : 0 < x) : ∑ s in nonzeroS D x, ψ D (D ^ (-s) * x) = 1 := by @@ -258,7 +255,7 @@ lemma mem_nonzeroS_iff {i : ℤ} {x : ℝ} (hx : 0 < x) : 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), - zpow_neg, ← rpow_intCast, ← rpow_intCast, lt_logb_iff_rpow_lt hD (four_x0 hx), + 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, Int.cast_one, rpow_neg (D0 hD).le, inv_lt_inv (four_x0 hx) (D_pow0 hD _), and_comm] @@ -331,8 +328,8 @@ lemma dist_mem_Icc_of_Ks_ne_zero {s : ℤ} {x y : X} (h : Ks s x y ≠ 0) : dist x y ∈ Icc ((D ^ (s - 1) : ℝ) / 4) (D ^ s / 2) := by simp only [Ks, Nat.cast_pow, Nat.cast_ofNat, zpow_neg, ne_eq, mul_eq_zero, ofReal_eq_zero] at h have dist_mem_Icc := Ioo_subset_Icc_self (support_ψ (D1 X) ▸ mem_support.2 (not_or.1 h).2) - rwa [mem_Icc, ← div_eq_inv_mul, le_div_iff (D_pow0' (D1 X) s), - div_le_iff (D_pow0' (D1 X) s), mul_inv, mul_assoc, inv_mul_eq_div (4 : ℝ), ← zpow_neg_one, + rwa [mem_Icc, ← div_eq_inv_mul, le_div_iff₀ (D_pow0' (D1 X) s), + div_le_iff₀ (D_pow0' (D1 X) s), mul_inv, mul_assoc, inv_mul_eq_div (4 : ℝ), ← zpow_neg_one, ← zpow_add₀ (D0' X).ne.symm, neg_add_eq_sub, ← div_eq_inv_mul] at dist_mem_Icc /-- The constant appearing in part 2 of Lemma 2.1.3. -/ @@ -346,7 +343,7 @@ lemma kernel_bound {s : ℤ} {x y : X} : change ‖K x y * ψ (D ^ (-s) * dist x y)‖ ≤ 2 ^ a ^ 3 / volume.real (ball x (dist x y)) apply le_trans <| calc ‖K x y * ψ (D ^ (-s) * dist x y)‖ - = ‖K x y‖ * ‖(ψ (D ^ (-s) * dist x y) : ℂ)‖ := by exact_mod_cast norm_mul _ _ + = ‖K x y‖ * ‖(ψ (D ^ (-s) * dist x y) : ℂ)‖ := norm_mul .. _ ≤ ‖K x y‖ * 1 := by gcongr; rw [norm_eq_abs, abs_ofReal]; exact abs_ψ_le_one D _ _ ≤ ‖K x y‖ := by rw [mul_one] convert norm_K_le_vol_inv (K := K) x y @@ -666,7 +663,7 @@ lemma integrable_Ks_x {s : ℤ} {x : X} (hD : 1 < (D : ℝ)) : Integrable (Ks s intro y hy rw [mem_support, ne_eq, ofReal_eq_zero, ← ne_eq, ← mem_support, support_ψ (D1 X)] at hy replace hy := le_of_lt hy.2 - rw [zpow_neg, mul_comm, ← div_eq_mul_inv, _root_.div_le_iff (Ds0 X s)] at hy + rw [zpow_neg, mul_comm, ← div_eq_mul_inv, div_le_iff₀ (Ds0 X s)] at hy rwa [mem_closedBall, dist_comm, div_eq_mul_inv, mul_comm] · refine Measurable.ite ?_ measurable_const measurable_K_right.of_uncurry_left convert measurableSet_closedBall (x := x) (ε := D ^ s / (4 * D)) diff --git a/Carleson/RealInterpolation.lean b/Carleson/RealInterpolation.lean index 04bf64df..a59cb59c 100644 --- a/Carleson/RealInterpolation.lean +++ b/Carleson/RealInterpolation.lean @@ -63,7 +63,7 @@ lemma biSup {ι : Type*} (𝓑 : Set ι) {T : ι → (α → E₁) → α' → by_cases A0 : A < 0 · refine SubadditiveOn.zero hP A (fun f hf ↦ funext fun x ↦ ?_) suffices ⨆ i ∈ 𝓑, T i f x = 0 by simp [this] - simp only [iSup_eq_zero] + simp only [ENNReal.iSup_eq_zero] intro i hi have := (toReal_eq_zero_iff _).mp (congr_fun ((h i hi).neg P A0 f hf) x) exact this.resolve_right (hT' i hi x f hf) @@ -128,7 +128,7 @@ lemma biSup {ι : Type*} (𝓑 : Set ι) (T : ι → (α → E₁) → α' → have := congr_fun ((h i hi).2 f c hf hc) x simp only [Pi.smul_apply, smul_eq_mul, ← toReal_ofReal_mul c (T i f x) hc] at this rw [ENNReal.toReal_eq_toReal (hT' i hi x (c • f) (h_smul hf hc)) - (mul_lt_top ofReal_ne_top (hT' i hi x f hf)).ne] at this + (mul_ne_top ofReal_ne_top (hT' i hi x f hf))] at this rwa [toReal_ofReal hc] lemma indicator {T : (α → E₁) → α' → E₂} {P : (α → E₁) → Prop} {A : ℝ} (S : Set α') diff --git a/Carleson/TileExistence.lean b/Carleson/TileExistence.lean index e1385866..9f5bcd8c 100644 --- a/Carleson/TileExistence.lean +++ b/Carleson/TileExistence.lean @@ -4,9 +4,6 @@ import Mathlib.Data.Set.Card import Mathlib.Data.Real.ENatENNReal import Mathlib.Data.Set.Subset --- https://github.com/leanprover/lean4/issues/4947 -attribute [-simp] Nat.reducePow - open Set MeasureTheory Metric Function Complex Bornology Notation open scoped NNReal ENNReal ComplexConjugate @@ -1470,7 +1467,7 @@ lemma const_n_prop_1 {t:ℝ} (ht:t∈Ioo 0 1) : D^(const_n a ht * K') ≤ t⁻¹ rw [← Real.rpow_logb (defaultD_pos a) (one_lt_realD X).ne.symm (inv_pos.mpr ht.left)] rw [← Real.rpow_natCast,Real.rpow_le_rpow_left_iff (one_lt_realD X)] simp only [Nat.cast_mul, Nat.cast_pow, Nat.cast_ofNat, Real.logb_inv] - rw [← le_div_iff (K_pos)] + rw [← le_div_iff₀ (K_pos)] rw [const_n] exact Nat.floor_le (prefloor_nonneg X ht) @@ -1487,7 +1484,7 @@ lemma const_n_is_max {t:ℝ} (ht:t∈Ioo 0 1) (n:ℕ) : D^(n * K') ≤ t⁻¹ rw [← Real.rpow_logb (defaultD_pos a) (one_lt_realD X).ne.symm (inv_pos.mpr ht.left)] rw [← Real.rpow_natCast,Real.rpow_le_rpow_left_iff (one_lt_realD X)] simp only [Nat.cast_mul, Nat.cast_pow, Nat.cast_ofNat, Real.logb_inv] - rw [← le_div_iff (K_pos)] + rw [← le_div_iff₀ (K_pos)] rw [const_n] intro h exact Nat.le_floor h @@ -1496,14 +1493,14 @@ variable (X) in lemma const_n_prop_3 {t:ℝ} (ht:t ∈ Ioo 0 1) : (t * D ^ K' : ℝ)⁻¹ ≤ ↑D ^ (const_n a ht * K') := by dsimp only [const_n] - rw [mul_inv,← div_eq_mul_inv,div_le_iff (pow_pos (defaultD_pos a) _), ← pow_add] + rw [mul_inv, ← div_eq_mul_inv, div_le_iff₀ (pow_pos (defaultD_pos a) _), ← pow_add] nth_rw 3 [← one_mul K'] rw [← right_distrib] nth_rw 1 [← Real.rpow_logb (defaultD_pos a) (one_lt_realD X).ne.symm ht.left] rw [← Real.rpow_neg (realD_nonneg)] rw [← Real.rpow_natCast,Real.rpow_le_rpow_left_iff (one_lt_realD X)] push_cast - rw [← div_le_iff (K_pos)] + rw [← div_le_iff₀ (K_pos)] apply LT.lt.le exact Nat.lt_floor_add_one (-Real.logb (↑D) t / ↑const_K) @@ -1611,8 +1608,8 @@ lemma boundary_measure {k:ℤ} (hk:-S ≤ k) (y:Yk X k) {t:ℝ≥0} (ht:t∈ Set apply ENNReal.add_lt_add_of_le_of_lt _ hxb' hxy' apply LT.lt.ne apply lt_of_le_of_lt hxb' - apply ENNReal.mul_lt_top (ENNReal.coe_ne_top) - apply (ENNReal.zpow_lt_top _ (ENNReal.natCast_ne_top D) _).ne + apply ENNReal.mul_lt_top ENNReal.coe_lt_top + apply ENNReal.zpow_lt_top _ (ENNReal.natCast_ne_top D) _ rw [ne_comm] apply LT.lt.ne rw [← ENNReal.ofReal_natCast] @@ -1869,7 +1866,7 @@ def grid_existence : GridStructure X D κ S o where · simp only [mem_Ioo] refine ⟨?_, ht'⟩ apply lt_of_lt_of_le (zpow_pos_of_pos (defaultD_pos a) _) ht - rw [zpow_sub₀, div_le_iff] at ht + rw [zpow_sub₀, div_le_iff₀] at ht · exact ht · exact zpow_pos_of_pos (defaultD_pos a) _ rw [ne_comm] @@ -2200,7 +2197,7 @@ lemma Ω_RFD {p q : 𝔓 X} (h𝓘 : 𝓘 p ≤ 𝓘 q) : Disjoint (Ω p) (Ω q) · exact Or.inr (key.trans c) termination_by (𝔰 q - 𝔰 p).toNat decreasing_by - simp_wf + rw [Int.lt_toNat] change (s J - 𝔰 p).toNat < 𝔰 q - 𝔰 p rw [sJ, Int.toNat_of_nonneg (by omega), sub_right_comm] exact sub_one_lt _ @@ -2219,3 +2216,5 @@ def tile_existence : TileStructure Q D κ S o where exact this.trans (Construction.ball_subset_Ω₁ p) · simp subset_cball {p} := Construction.Ω_subset_cball + +set_option linter.style.longFile 2400 diff --git a/Carleson/TileStructure.lean b/Carleson/TileStructure.lean index 0e6af853..e548c9d9 100644 --- a/Carleson/TileStructure.lean +++ b/Carleson/TileStructure.lean @@ -1,9 +1,6 @@ import Carleson.GridStructure import Carleson.Psi --- https://github.com/leanprover/lean4/issues/4947 -attribute [-simp] Nat.reducePow - open Set MeasureTheory Metric Function Complex Bornology open scoped NNReal ENNReal ComplexConjugate noncomputable section diff --git a/Carleson/ToMathlib/Height.lean b/Carleson/ToMathlib/Height.lean index a2181641..58df3f76 100644 --- a/Carleson/ToMathlib/Height.lean +++ b/Carleson/ToMathlib/Height.lean @@ -3,8 +3,8 @@ Copyright (c) 2024 Joachim Breitner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joachim Breitner -/ -import Mathlib.Order.RelSeries import Mathlib.Data.ENat.Lattice +import Mathlib.Order.RelSeries /-! # Height of an element in a partial order @@ -100,12 +100,6 @@ lemma ENat.isup_add (ι : Type*) [Nonempty ι] (f : ι → ℕ∞) (n : ℕ∞) variable {α : Type*} -lemma RelSeries.eraseLast_last_rel_last {r : Rel α α} (p : RelSeries r) (h : 0 < p.length) : - r p.eraseLast.last p.last := by - simp only [last, Fin.last, eraseLast_length, eraseLast_toFun] - convert p.step ⟨p.length -1, by omega⟩ - simp; omega - /-- Replaces the last element in a series. Essentially `p.eraseLast.snoc x`, but also works when `p` is a singleton. -/ def LTSeries.replaceLast [Preorder α] (p : LTSeries α) (x : α) (h : p.last ≤ x) : @@ -129,9 +123,6 @@ lemma LTSeries.length_replaceLast [Preorder α] (p : LTSeries α) (x : α) (h : (p.replaceLast x h).length = p.length := by unfold replaceLast; split <;> (simp;omega) -lemma LTSeries.head_le_last [Preorder α] (p : LTSeries α) : p.head ≤ p.last := - LTSeries.monotone p (Fin.zero_le (Fin.last p.length)) - lemma LTSeries.int_head_add_le_toFun (p : LTSeries ℤ) (i : Fin (p.length + 1)) : p.head + i ≤ p i := by have ⟨i, hi⟩ := i simp only @@ -274,7 +265,7 @@ lemma coe_lt_height_iff (x : α) (n : ℕ) (hfin : height x < ⊤): constructor · intro h obtain ⟨m, hx : height x = m⟩ := Option.ne_none_iff_exists'.mp (LT.lt.ne_top hfin) - rw [hx] at h; norm_num at h + rw [hx, Nat.cast_lt] at h obtain ⟨p, hp, hlen⟩ := exists_series_of_height_eq_coe x hx use p ⟨n, by omega⟩ constructor @@ -314,10 +305,6 @@ lemma height_eq_coe_iff (x : α) (n : ℕ) : rename_i y _ cases height y <;> simp ; norm_cast; omega -/-- Probably redundant -/ -theorem minimal_iff_forall_lt_not_mem {x : α} {s : Set α} : - Minimal (· ∈ s) x ↔ x ∈ s ∧ ∀ ⦃y⦄, y < x → y ∉ s := minimal_iff_forall_lt - lemma minimal_iff_height_eq_zero (a : α) : Minimal (fun _ ↦ True) a ↔ height a = 0 := by simp [minimal_iff_forall_lt, height_eq_zero_iff] diff --git a/Carleson/ToMathlib/MeasureReal.lean b/Carleson/ToMathlib/MeasureReal.lean index 792c3af8..ad7cac16 100644 --- a/Carleson/ToMathlib/MeasureReal.lean +++ b/Carleson/ToMathlib/MeasureReal.lean @@ -278,7 +278,7 @@ lemma measureReal_symmDiff_eq (hs : MeasurableSet s) (ht : MeasurableSet t) (h₁ : μ s ≠ ∞ := by finiteness) (h₂ : μ t ≠ ∞ := by finiteness) : μ.real (s ∆ t) = μ.real (s \ t) + μ.real (t \ s) := by simp only [Measure.real] - rw [← ENNReal.toReal_add, measure_symmDiff_eq hs ht] + rw [← ENNReal.toReal_add, measure_symmDiff_eq hs.nullMeasurableSet ht.nullMeasurableSet] · exact measure_ne_top_of_subset diff_subset h₁ · exact measure_ne_top_of_subset diff_subset h₂ @@ -430,7 +430,7 @@ theorem exists_nonempty_inter_of_measureReal_univ_lt_sum_measureReal · convert H rw [ENNReal.toReal_sum (fun i hi ↦ measure_ne_top _ _)] rfl - · exact (ENNReal.sum_lt_top (fun i hi ↦ measure_ne_top _ _)).ne + · exact (ENNReal.sum_lt_top.mpr (fun i hi ↦ measure_lt_top _ _)).ne /-- If two sets `s` and `t` are included in a set `u` of finite measure, and `μ.real s + μ.real t > μ.real u`, then `s` intersects `t`. diff --git a/Carleson/WeakType.lean b/Carleson/WeakType.lean index 9fc627e9..2ff1bce1 100644 --- a/Carleson/WeakType.lean +++ b/Carleson/WeakType.lean @@ -218,12 +218,12 @@ lemma lintegral_norm_pow_eq_distribution {p : ℝ} (hp : 0 < p) : ∫⁻ t in Ioi (0 : ℝ), ENNReal.ofReal (p * t ^ (p - 1)) * distribution f (.ofReal t) μ := by have h2p : 0 ≤ p := hp.le have := MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul μ (f := fun x ↦ ‖f x‖) - (eventually_of_forall fun x ↦ norm_nonneg _) hf.norm hp + (Eventually.of_forall fun x ↦ norm_nonneg _) hf.norm hp simp [*, ENNReal.coe_rpow_of_nonneg, ← ENNReal.ofReal_rpow_of_nonneg, ← ofReal_norm_eq_coe_nnnorm, ofReal_mul, ← lintegral_const_mul', ← mul_assoc, mul_comm (μ _), distribution] at this ⊢ convert this using 1 - refine setLIntegral_congr_fun measurableSet_Ioi (eventually_of_forall fun x hx ↦ ?_) + refine setLIntegral_congr_fun measurableSet_Ioi (Eventually.of_forall fun x hx ↦ ?_) simp_rw [ENNReal.ofReal_lt_ofReal_iff_of_nonneg (le_of_lt hx)] /-- The layer-cake theorem, or Cavalieri's principle, written using `eLpNorm`. -/ diff --git a/lake-manifest.json b/lake-manifest.json index d7be4ff1..f93bbf6c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ad26fe1ebccc9d5b7ca9111d5daf9b4488374415", + "rev": "8feac540abb781cb1349688c816dc02fae66b49c", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222", + "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "776a5a8f9c789395796e442d78a9d4cb9c4c9d03", + "rev": "e291aa4de57079b3d2199b9eb7b4b00922b85a7c", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,10 +35,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a96aee5245720f588876021b6a0aa73efee49c76", + "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.41", + "inputRev": "v0.0.42", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6", + "rev": "3e96ea03edd48b932566ca9b201285ae2d57130d", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "08570c45d1aa03a1fbd90726896570534d03275f", + "rev": "df80b0dd2548c76fbdc3fe5d3a96873dfd46c0dc", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "21a36f3c07a9229e1287483c16a0dd04e479ecc5", + "rev": "11fa569b1b52f987dc5dcea97fd80eaff95c2fce", "name": "checkdecls", "manifestFile": "lake-manifest.json", "inputRev": "master", diff --git a/lean-toolchain b/lean-toolchain index e7a4f40b..98556ba0 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.11.0-rc2 +leanprover/lean4:v4.12.0-rc1