Complex.CartanBound.log_norm_one_sub_div_ge_neg_phi
PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanBound.lean:219 to 264
Source documentation
The one-dimensional logarithmic singularity used in the Cartan/dyadic averaging argument. -/ noncomputable def φ (t : ℝ) : ℝ := log⁺ (1 / |1 - t|)
lemma measurable_phi : Measurable φ := by unfold φ simpa [Real.posLog_def, Real.posLog] using (by fun_prop : Measurable fun t : ℝ => max 0 (Real.log (1 / |1 - t|)))
lemma phi_le_log_two_of_le_half {t : ℝ} (ht : t ≤ (1 / 2 : ℝ)) : φ t ≤ Real.log 2 := by have hnonneg : 0 ≤ (1 - t : ℝ) := by linarith have hden : (1 / 2 : ℝ) ≤ |1 - t| := by have : (1 / 2 : ℝ) ≤ (1 - t : ℝ) := by linarith simpa [abs_of_nonneg hnonneg] using this have hfrac : (1 / |1 - t| : ℝ) ≤ 2 := by have hhalfpos : (0 : ℝ) < (1 / 2 : ℝ) := by norm_num have := one_div_le_one_div_of_le hhalfpos hden simpa [one_div, div_eq_mul_inv] using this have hposLog : log⁺ (1 / |1 - t|) ≤ log⁺ (2 : ℝ) := Real.posLog_le_posLog (by positivity) hfrac have habs : (1 : ℝ) ≤ |(2 : ℝ)| := by simp have hposLog2 : (log⁺ (2 : ℝ)) = Real.log 2 := by simpa using (Real.posLog_eq_log habs) simpa [φ, hposLog2] using hposLog
lemma phi_eq_zero_of_one_le_abs_one_sub {t : ℝ} (ht : (1 : ℝ) ≤ |1 - t|) : φ t = 0 := by have hpos : 0 < |1 - t| := lt_of_lt_of_le (by norm_num) ht have hfrac : (1 / |1 - t| : ℝ) ≤ 1 := (div_le_one hpos).2 ht have habs : |(1 / |1 - t| : ℝ)| ≤ 1 := by have hnonneg : 0 ≤ (1 / |1 - t| : ℝ) := by positivity simpa [abs_of_nonneg hnonneg] using hfrac have : log⁺ (1 / |1 - t|) = 0 := (Real.posLog_eq_zero_iff _).2 habs simpa [φ] using this
lemma φ_nonneg (t : ℝ) : 0 ≤ φ t := by simpa [φ] using (Real.posLog_nonneg (x := (1 / |1 - t|)))
lemma φ_le_sqrt (t : ℝ) : φ t ≤ Real.sqrt (2 / |1 - t|) := by simpa [φ, Real.posLog] using posLog_log_one_div_abs_one_sub_le_sqrt (t := t)
lemma ae_restrict_norm_phi_le_of_forall_mem {A B : ℝ} (hAB : A ≤ B) {g : ℝ → ℝ} (hg : ∀ t, 0 ≤ g t) (h : ∀ t ∈ Set.Icc A B, φ t ≤ g t) : (fun t : ℝ => ‖φ t‖) ≤ᶠ[ae (volume.restrict (Set.uIoc A B))] fun t => ‖g t‖ := by refine MeasureTheory.ae_restrict_of_forall_mem (μ := (volume : MeasureTheory.Measure ℝ)) (s := Set.uIoc A B) (by simpa using (measurableSet_uIoc : MeasurableSet (Set.uIoc A B))) ?_ intro t ht have htIoc : t ∈ Set.Ioc A B := by simpa [Set.uIoc_of_le hAB] using ht have htIcc : t ∈ Set.Icc A B := ⟨le_of_lt htIoc.1, htIoc.2⟩ have hle : φ t ≤ g t := h t htIcc have hφ0 : 0 ≤ φ t := φ_nonneg t have hg0 : 0 ≤ g t := hg t simpa [Real.norm_eq_abs, abs_of_nonneg hφ0, abs_of_nonneg hg0] using hle
/-!
Bridge lemma: from the 1D singularity φ to a complex lower bound
On a circle ‖u‖ = r, the quantity log ‖1 - u/a‖ is bounded below in terms of φ(r/‖a‖).
This is the local estimate in the probabilistic-radius argument.
Exact Lean statement
lemma log_norm_one_sub_div_ge_neg_phi {u a : ℂ} {r : ℝ}
(hur : ‖u‖ = r) (ha : a ≠ 0) (hr : r ≠ ‖a‖) :
Real.log ‖(1 : ℂ) - u / a‖ ≥ -φ (r / ‖a‖)Complete declaration
Lean source
lemma log_norm_one_sub_div_ge_neg_phi {u a : ℂ} {r : ℝ} (hur : ‖u‖ = r) (ha : a ≠ 0) (hr : r ≠ ‖a‖) : Real.log ‖(1 : ℂ) - u / a‖ ≥ -φ (r / ‖a‖) := by have ha_norm : 0 < ‖a‖ := norm_pos_iff.2 ha have hnorm_eq : ‖(1 : ℂ) - u / a‖ = ‖a - u‖ / ‖a‖ := by have : (1 : ℂ) - u / a = (a - u) / a := by field_simp [ha] calc ‖(1 : ℂ) - u / a‖ = ‖(a - u) / a‖ := by simp [this] _ = ‖a - u‖ / ‖a‖ := by simp have hrev : |‖a‖ - ‖u‖| ≤ ‖a - u‖ := by simpa using (abs_norm_sub_norm_le a u) have hdiv : |‖a‖ - ‖u‖| / ‖a‖ ≤ ‖a - u‖ / ‖a‖ := div_le_div_of_nonneg_right hrev (le_of_lt ha_norm) have habs : |1 - (r / ‖a‖)| = |‖a‖ - ‖u‖| / ‖a‖ := by have hu : ‖u‖ = r := hur have ha0 : (‖a‖ : ℝ) ≠ 0 := ha_norm.ne' have h1 : (1 : ℝ) - (r / ‖a‖) = (‖a‖ - r) / ‖a‖ := by field_simp [ha0] calc |1 - (r / ‖a‖)| = |(‖a‖ - r) / ‖a‖| := by simp [h1] _ = |‖a‖ - r| / ‖a‖ := by simp [abs_div, abs_of_pos ha_norm] _ = |‖a‖ - ‖u‖| / ‖a‖ := by simp [hu] have hnorm_ge : |1 - (r / ‖a‖)| ≤ ‖(1 : ℂ) - u / a‖ := by have : |1 - (r / ‖a‖)| ≤ ‖a - u‖ / ‖a‖ := by rw [habs] exact hdiv rwa [hnorm_eq] have hx0 : 0 < |1 - (r / ‖a‖)| := by have : (1 - (r / ‖a‖) : ℝ) ≠ 0 := by intro h0 have : r = ‖a‖ := by have : r / ‖a‖ = (1 : ℝ) := by linarith simpa using (div_eq_iff ha_norm.ne').1 this exact hr this have : |1 - (r / ‖a‖)| ≠ 0 := by simpa [abs_eq_zero] using this exact lt_of_le_of_ne (abs_nonneg _) (Ne.symm this) have hlogx : Real.log |1 - (r / ‖a‖)| ≥ -φ (r / ‖a‖) := by have := Real.neg_posLog_inv_le_log (x := |1 - (r / ‖a‖)|) simpa [φ, one_div, inv_inv, abs_sub_comm, sub_eq_add_neg] using this have hlog_mono : Real.log |1 - (r / ‖a‖)| ≤ Real.log ‖(1 : ℂ) - u / a‖ := Real.log_le_log (by positivity) hnorm_ge linarith [hlog_mono, hlogx]