PL1/DyadicInterpolationNormComparison.lean

All source files · Download exact source

SHA-256: da5594716658b1612dc31f365e1f7ebdf7c219e9b2cdce31d4e1d8bf729ca8a7

1import PL1.DyadicInterpolationIntegral2import Mathlib.Tactic.GCongr34/-! Explicit universal constants for the dyadic interpolation comparison. -/56noncomputable section7open MeasureTheory Filter Set8open scoped ENNReal Topology910namespace PL1.DyadicInterpolation1112theorem weight_eq_sqrt_two_pow (n : ℕ) : weight n = (Real.sqrt 2) ^ n := by13  have hh : (1 / 2 : ℝ) ^ (-1 / 2 : ℝ) = Real.sqrt 2 := by14    rw [show (-1 / 2 : ℝ) = -(1 / 2) by ring, Real.rpow_neg_eq_inv_rpow]15    norm_num [Real.sqrt_eq_rpow]16  induction n with17  | zero => simp [weight]18  | succ n ih => rw [weight_succ, ih, hh, pow_succ]1920theorem quarter_le_lowerConstant : (1 / 4 : ℝ) ≤ lowerConstant := by21  have h := Real.rpow_le_rpow_of_exponent_ge (by norm_num : (0 : ℝ) < 1 / 2)22    (by norm_num : (1 / 2 : ℝ) ≤ 1) (by norm_num : (1 / 2 : ℝ) ≤ 1)23  rw [Real.rpow_one] at h24  unfold lowerConstant25  linarith2627theorem upperConstant_le_two : upperConstant ≤ 2 := by28  have h := Real.rpow_le_rpow_of_exponent_ge (by norm_num : (0 : ℝ) < 1 / 2)29    (by norm_num : (1 / 2 : ℝ) ≤ 1) (by norm_num : (-2 : ℝ) ≤ -3 / 2)30  norm_num [Real.rpow_neg_natCast] at h31  unfold upperConstant32  linarith3334@[simp] theorem sample_zero (k : ℝ → ℝ) : sample k 0 = ENNReal.ofReal (k 1) := by35  simp [sample, weight]3637def discreteNorm (k : ℝ → ℝ) : ℝ≥0∞ := ENNReal.ofReal (k 1) + ∑' n, sample k (n + 1)3839theorem discreteNorm_eq_tsum (k : ℝ → ℝ) : discreteNorm k = ∑' n, sample k n := by40  rw [tsum_eq_zero_add' ENNReal.summable, sample_zero]41  rfl4243variable {k : ℝ → ℝ}4445theorem fullIntegral_le_four_discreteNorm (hk : ∀ t ∈ Ici (0 : ℝ), 0 ≤ k t)46    (hmono : MonotoneOn k (Ici (0 : ℝ)))47    (htail : ∀ t, 1 ≤ t → k t = k 1) :48    fullIntegral k ≤ 4 * discreteNorm k := by49  have hu : smallIntegral k ≤ 2 * discreteNorm k := by50    calc51      _ ≤ ENNReal.ofReal upperConstant * discreteNorm k := by52        rw [discreteNorm_eq_tsum]53        exact (smallIntegral_bounds hk hmono).254      _ ≤ 2 * discreteNorm k := by55        gcongr56        exact_mod_cast ENNReal.ofReal_le_ofReal upperConstant_le_two57  have hz : ENNReal.ofReal (k 1) ≤ discreteNorm k := le_self_add58  rw [fullIntegral_eq (hk 1 (by norm_num)) htail,59    ENNReal.ofReal_mul (by norm_num : (0 : ℝ) ≤ 2)]60  norm_num only [ENNReal.ofReal_ofNat]61  calc62    _ ≤ 2 * discreteNorm k + 2 * discreteNorm k := add_le_add hu (by gcongr)63    _ = 4 * discreteNorm k := by rw [← add_mul]; norm_num6465theorem discreteNorm_le_five_fullIntegral (hk : ∀ t ∈ Ici (0 : ℝ), 0 ≤ k t)66    (hmono : MonotoneOn k (Ici (0 : ℝ)))67    (htail : ∀ t, 1 ≤ t → k t = k 1) :68    discreteNorm k ≤ 5 * fullIntegral k := by69  have hs : smallIntegral k ≤ fullIntegral k := by70    rw [fullIntegral_eq (hk 1 (by norm_num)) htail]71    exact le_self_add72  have hl : (1 / 4 : ℝ≥0∞) * (∑' n, sample k (n + 1)) ≤ fullIntegral k := by73    calc74      _ ≤ ENNReal.ofReal lowerConstant * (∑' n, sample k (n + 1)) := by75        gcongr76        have h := ENNReal.ofReal_le_ofReal quarter_le_lowerConstant77        simpa only [ENNReal.ofReal_div_of_pos (by norm_num : (0 : ℝ) < 4),78          ENNReal.ofReal_one, ENNReal.ofReal_ofNat] using h79      _ ≤ smallIntegral k := (smallIntegral_bounds hk hmono).180      _ ≤ fullIntegral k := hs81  have hsum : (∑' n, sample k (n + 1)) ≤ 4 * fullIntegral k := by82    have h : 4 * ((1 / 4 : ℝ≥0∞) * (∑' n, sample k (n + 1))) ≤ 4 * fullIntegral k := by83      gcongr84    simpa only [← mul_assoc, one_div,85      ENNReal.mul_inv_cancel (by norm_num : (4 : ℝ≥0∞) ≠ 0) (by finiteness : (4 : ℝ≥0∞) ≠ ⊤),86      one_mul] using h87  have hz : ENNReal.ofReal (k 1) ≤ fullIntegral k := by88    calc89      _ ≤ ENNReal.ofReal (2 * k 1) := ENNReal.ofReal_le_ofReal (by nlinarith [hk 1 (by norm_num)])90      _ ≤ fullIntegral k := by91        rw [fullIntegral_eq (hk 1 (by norm_num)) htail]92        exact le_add_self93  unfold discreteNorm94  calc95    _ ≤ fullIntegral k + 4 * fullIntegral k := add_le_add hz hsum96    _ = (1 + 4) * fullIntegral k := by rw [add_mul, one_mul]97    _ = 5 * fullIntegral k := by norm_num9899theorem fullIntegral_ne_top_iff_discreteNorm (hk : ∀ t ∈ Ici (0 : ℝ), 0 ≤ k t)100    (hmono : MonotoneOn k (Ici (0 : ℝ)))101    (htail : ∀ t, 1 ≤ t → k t = k 1) :102    fullIntegral k ≠ ⊤ ↔ discreteNorm k ≠ ⊤ := by103  rw [fullIntegral_ne_top_iff hk hmono htail, discreteNorm, ENNReal.add_ne_top]104  exact (and_iff_right ENNReal.ofReal_ne_top).symm105106end PL1.DyadicInterpolation107