Source indexedlemma · leanprover/lean4:v4.32.0

exists_uniform_annulus_bound

Carleson.MetricCarleson.Truncation · Carleson/MetricCarleson/Truncation.lean:422 to 443

Source documentation

There exists a uniform bound for all possible values of L302 and U302 over the annulus in R_truncation.

Exact Lean statement

lemma exists_uniform_annulus_bound {R : ℝ} (hR : 0 < R) :
    ∃ B : ℕ, ∀ R₁ ∈ Ioo R⁻¹ R, ∀ R₂ ∈ Ioo R₁ R,
      L302 a R₁ ∈ Finset.Icc (-B : ℤ) B ∧ U302 a R₂ ∈ Finset.Icc (-B : ℤ) B

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma exists_uniform_annulus_bound {R : ℝ} (hR : 0 < R) :    ∃ B : ℕ, ∀ R₁ ∈ Ioo R⁻¹ R, ∀ R₂ ∈ Ioo R₁ R,      L302 a R₁ ∈ Finset.Icc (-B : ℤ) B ∧ U302 a R₂ ∈ Finset.Icc (-B : ℤ) B := by  have iRpos : 0 < R⁻¹ := by positivity  let B₁ := (L302 a R⁻¹).natAbs  let B₂ := (L302 a R).natAbs  let B₃ := (U302 a R⁻¹).natAbs  let B₄ := (U302 a R).natAbs  use max (max B₁ B₂) (max B₃ B₄); intro R₁ mR₁ R₂ mR₂  have R₁pos : 0 < R₁ := iRpos.trans mR₁.1  have R₂pos : 0 < R₂ := R₁pos.trans mR₂.1  constructor  · suffices L302 a R₁ ∈ Finset.Icc (-B₁ : ℤ) B₂ by rw [Finset.mem_Icc] at this ⊢; omega    simp_rw [Finset.mem_Icc, B₁, B₂]    have h₁ : L302 a R⁻¹ ≤ L302 a R₁ := monotoneOn_L302 (X := X) iRpos R₁pos mR₁.1.le    have h₂ : L302 a R₁ ≤ L302 a R := monotoneOn_L302 (X := X) R₁pos hR mR₁.2.le    lia  · suffices U302 a R₂ ∈ Finset.Icc (-B₃ : ℤ) B₄ by rw [Finset.mem_Icc] at this ⊢; omega    simp_rw [Finset.mem_Icc, B₃, B₄]    have h₃ : U302 a R⁻¹ ≤ U302 a R₂ := monotoneOn_U302 (X := X) iRpos R₂pos (mR₁.1.trans mR₂.1).le    have h₄ : U302 a R₂ ≤ U302 a R := monotoneOn_U302 (X := X) R₂pos hR mR₂.2.le    lia