PL1/CarrierAsymptotics.lean
All source files · Download exact source
SHA-256: 2964a61894ac94c04ea9492523d90a37caff640e1df9959c44cf9f463341473c
1import Mathlib.Analysis.SpecialFunctions.Exp2import Mathlib.Analysis.SpecialFunctions.Log.Basic3import Mathlib.Analysis.SpecialFunctions.Sqrt4import Mathlib.Analysis.Normed.Group.InfiniteSum5import Mathlib.Tactic.FieldSimp6import Mathlib.Tactic.Linarith7import Mathlib.Tactic.Ring89/-!10# Scalar estimates for the common singular carrier1112The dyadic thresholds and square-root logarithmic bias lower bounds used in13the Borel--Cantelli construction, including arbitrary nonnegative tail shifts.14-/1516noncomputable section17set_option maxHeartbeats 80000018open Filter19open scoped Topology2021namespace PL1.CarrierAsymptotics2223def threshold (r : ℕ) : ℝ := (Real.exp (-Real.log 2 / 4)) ^ r2425def biasLower (u c : ℝ) (r : ℕ) : ℝ :=26 Real.exp (-u * Real.sqrt (((r : ℝ) + c) * Real.log 2))2728theorem log_two_pos : 0 < Real.log 2 := Real.log_pos (by norm_num)2930theorem threshold_pos (r : ℕ) : 0 < threshold r := pow_pos (Real.exp_pos _) _3132theorem biasLower_pos (u c : ℝ) (r : ℕ) : 0 < biasLower u c r := Real.exp_pos _3334/-- A fixed square-root logarithmic bias exponent grows slower than every35positive linear function of the dyadic index. -/36theorem eventually_sqrt_le_linear (u : ℝ) (hu : 0 ≤ u) (c : ℝ) (hc : 0 ≤ c)37 (ε : ℝ) (hε : 0 < ε) :38 ∀ᶠ r : ℕ in atTop, u * Real.sqrt (((r : ℝ) + c) * Real.log 2) ≤ ε * r := by39 have h₁ : ∀ᶠ r : ℕ in atTop, c ≤ (r : ℝ) := (eventually_ge_atTop c).natCast_atTop40 have h₂ : ∀ᶠ r : ℕ in atTop, 2 * u ^ 2 * Real.log 2 / ε ^ 2 ≤ (r : ℝ) :=41 (eventually_ge_atTop (2 * u ^ 2 * Real.log 2 / ε ^ 2)).natCast_atTop42 filter_upwards [h₁, h₂] with r hrc hrbound43 have hr : 0 ≤ (r : ℝ) := Nat.cast_nonneg r44 have hscale : 2 * u ^ 2 * Real.log 2 ≤ ε ^ 2 * r :=45 (div_le_iff₀ (sq_pos_of_pos hε)).1 hrbound |>.trans_eq (mul_comm _ _)46 have harg : 0 ≤ ((r : ℝ) + c) * Real.log 2 :=47 mul_nonneg (add_nonneg hr hc) log_two_pos.le48 have hs := Real.sq_sqrt harg49 have hsq : (u * Real.sqrt (((r : ℝ) + c) * Real.log 2)) ^ 2 =50 u ^ 2 * (((r : ℝ) + c) * Real.log 2) := by rw [mul_pow, hs]51 have hsum : ((r : ℝ) + c) * Real.log 2 ≤ 2 * r * Real.log 2 := by52 nlinarith [log_two_pos]53 have hleft := mul_le_mul_of_nonneg_left hsum (sq_nonneg u)54 have hright := mul_le_mul_of_nonneg_right hscale hr55 have hlinear : 0 ≤ ε * (r : ℝ) := mul_nonneg hε.le hr56 have hsqrt : 0 ≤ u * Real.sqrt (((r : ℝ) + c) * Real.log 2) :=57 mul_nonneg hu (Real.sqrt_nonneg _)58 nlinarith5960theorem threshold_eq_exp (r : ℕ) :61 threshold r = Real.exp ((r : ℝ) * (-Real.log 2 / 4)) := by62 exact (Real.exp_nat_mul (-Real.log 2 / 4) r).symm6364/-- The bias lower bound eventually exceeds twice the carrier threshold. -/65theorem eventually_two_threshold_le_biasLower (u : ℝ) (hu : 0 ≤ u) (c : ℝ) (hc : 0 ≤ c) :66 ∀ᶠ r : ℕ in atTop, 2 * threshold r ≤ biasLower u c r := by67 have hε : 0 < Real.log 2 / 8 := div_pos log_two_pos (by norm_num)68 have hg := eventually_sqrt_le_linear u hu c hc (Real.log 2 / 8) hε69 filter_upwards [hg, (eventually_ge_atTop (8 : ℝ)).natCast_atTop] with r hr hr870 rw [threshold_eq_exp, ← Real.exp_log (by norm_num : (0 : ℝ) < 2), ← Real.exp_add]71 apply Real.exp_le_exp.272 rw [Real.log_exp]73 change Real.log 2 + (r : ℝ) * (-Real.log 2 / 4) ≤ -u * Real.sqrt (((r : ℝ) + c) * Real.log 2)74 nlinarith [log_two_pos]7576theorem half_pow_eq_exp (r : ℕ) :77 (1 / 2 : ℝ) ^ r = Real.exp ((r : ℝ) * (-Real.log 2)) := by78 rw [Real.exp_nat_mul, Real.exp_neg, Real.exp_log (by norm_num : (0 : ℝ) < 2)]79 rw [one_div]8081/-- The summable Chebyshev bounds for all fixed positive-time noise laws. -/82theorem summable_noise_failure_bound (u : ℝ) (hu : 0 ≤ u) (c : ℝ) (hc : 0 ≤ c) :83 Summable (fun r : ℕ => 4 * (1 / 2 : ℝ) ^ r *84 Real.exp (2 * u * Real.sqrt (((r : ℝ) + c) * Real.log 2))) := by85 have hgeom : Summable (fun r : ℕ => 4 * Real.exp ((r : ℝ) * (-Real.log 2 / 2))) :=86 (Real.summable_exp_nat_mul_iff.2 (by linarith [log_two_pos])).mul_left 487 apply hgeom.of_norm_bounded_eventually_nat88 have hg := eventually_sqrt_le_linear u hu c hc (Real.log 2 / 4)89 (div_pos log_two_pos (by norm_num))90 filter_upwards [hg] with r hr91 rw [Real.norm_eq_abs, abs_of_nonneg (by positivity)]92 rw [half_pow_eq_exp, mul_assoc, ← Real.exp_add]93 apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : ℝ) ≤ 4)94 apply Real.exp_le_exp.295 nlinarith9697/-- The Haar Chebyshev bounds form a convergent geometric series. -/98theorem summable_haar_failure_bound :99 Summable (fun r : ℕ => (1 / 2 : ℝ) ^ r / (threshold r) ^ 2) := by100 have hg : Summable (fun r : ℕ => Real.exp ((r : ℝ) * (-Real.log 2 / 2))) :=101 Real.summable_exp_nat_mul_iff.2 (by linarith [log_two_pos])102 apply hg.congr103 intro r104 rw [threshold_eq_exp, half_pow_eq_exp, ← Real.exp_nat_mul, ← Real.exp_sub]105 congr 1106 push_cast107 ring108109/-- The slow rates remain controlled after deleting an arbitrary finite prefix. -/110theorem shifted_rate_le (d r j : ℕ) (hj : j < 2 ^ r) :111 Real.sqrt (Real.log ((d + j : ℕ) + 2 : ℝ)) ≤112 Real.sqrt (((r : ℝ) + (d : ℝ) + 1) * Real.log 2) := by113 have hd : d + 2 ≤ 2 ^ (d + 1) := by114 have h : d + 1 < 2 ^ (d + 1) := Nat.lt_two_pow_self115 omega116 have hr : 1 ≤ (2 : ℕ) ^ r := Nat.one_le_two_pow117 have hn : d + j + 2 ≤ 2 ^ (r + d + 1) := by118 calc119 d + j + 2 ≤ d + 2 ^ r + 1 := by omega120 _ ≤ (d + 2) * 2 ^ r := by nlinarith121 _ ≤ 2 ^ (d + 1) * 2 ^ r := Nat.mul_le_mul_right _ hd122 _ = 2 ^ (r + d + 1) := by rw [← pow_add]; congr 1; omega123 have hcast : ((d + j : ℕ) + 2 : ℝ) ≤ (2 : ℝ) ^ (r + d + 1) := by exact_mod_cast hn124 apply Real.sqrt_le_sqrt125 calc126 _ ≤ Real.log ((2 : ℝ) ^ (r + d + 1)) := Real.log_le_log (by positivity) hcast127 _ = _ := by rw [Real.log_pow]; push_cast; ring128129theorem noise_failure_bound_eq (u c : ℝ) (r : ℕ) :130 (1 / 2 : ℝ) ^ r / (biasLower u c r / 2) ^ 2 =131 4 * (1 / 2 : ℝ) ^ r * Real.exp (2 * u * Real.sqrt (((r : ℝ) + c) * Real.log 2)) := by132 unfold biasLower133 have he : Real.exp (2 * u * Real.sqrt (((r : ℝ) + c) * Real.log 2)) =134 (Real.exp (-u * Real.sqrt (((r : ℝ) + c) * Real.log 2)) ^ 2)⁻¹ := by135 rw [← Real.exp_nat_mul, ← Real.exp_neg]136 congr 1137 push_cast138 ring139 rw [he]140 field_simp141 norm_num142143end PL1.CarrierAsymptotics144