SmallImageSector.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The central-sector extension of es:good-semicircle. The already proved omitted-value estimate gives a universal constant 4096 * π in place of the sharper constant 6 in the manuscript; this suffices for the splice.

lemma OAI.SLEExactGauge.SmallImageSemicircle.log_norm_fderiv_le_of_height line 18

theorem OAI.SLEExactGauge.SmallImageSemicircle.central_sector_log_bound line 50

Source documentation

Uniform comparison with the top of the selected semicircle on the central sector. The straight segment stays above height B/16.

theorem central_sector_log_bound
    {F : ℂ → ℂ} (hF : DifferentiableOn ℂ F {z | 0 < z.im})
    (hi : InjOn F {z | 0 < z.im}) {a : ℂ}
    (ha : ∀ z, 0 < z.im → F z ≠ a) {B : ℝ} (hB : 0 < B)
    {z : ℂ} (hzlow : B / 8 ≤ ‖z‖) (hzup : ‖z‖ ≤ B)
    (hzim : ‖z‖ / 2 ≤ z.im) :
    Real.log ‖F z - a‖ ≤ Real.log ‖F ((B : ℂ) * Complex.I) - a‖ + 4096 * Real.pi := by
…

theorem OAI.SLEExactGauge.SmallImageSemicircle.central_sector_norm_bound line 89

theorem OAI.SLEExactGauge.SmallImageSemicircle.exists_arbitrarily_small_image_sector line 106

Source documentation

Semicircles and their central sectors can be made arbitrarily small in parameter space while preserving a uniform image bound.

theorem exists_arbitrarily_small_image_sector
    {F : ℂ → ℂ} (hF : DifferentiableOn ℂ F {z | 0 < z.im})
    (hi : InjOn F {z | 0 < z.im}) {a : ℂ}
    (ha : ∀ z, 0 < z.im → F z ≠ a) {r A t₀ : ℝ} {β : ℝ → ℂ}
    (hr : 0 < r) (hA : 2 * Real.pi ^ 2 < A)
    (ht₀ : 0 < t₀) (hβ : ContinuousOn β (Icc 0 t₀)) (hβ₀ : β 0 = 0)
    (hβH : ∀ t ∈ Ioc 0 t₀, 0 < (β t).im)
    (hsmall : ∀ t ∈ Ioc 0 t₀, ‖F (β t) - a‖ ≤ r * Real.exp (-A)) :
    ∀ δ : ℝ, 0 < δ → ∃ B ∈ Ioo 0 δ,
      (∀ θ ∈ Ioo 0 Real.pi,
        ‖F ((B : ℂ) * Complex.exp ((θ : ℂ) * Complex.I)) - a‖ ≤
          r * Real.exp (-A + Real.pi * Real.sqrt (2 * A))) ∧
…

lemma OAI.SLEExactGauge.SmallImageSemicircle.sector_exponential_lt_quarter line 134

theorem OAI.SLEExactGauge.SmallImageSemicircle.exists_arbitrarily_small_quarter_image_sector line 157

Source documentation

A fixed sufficiently deep guide segment provides the small semicircle and central sector used to splice the initial passage.

theorem exists_arbitrarily_small_quarter_image_sector
    {F : ℂ → ℂ} (hF : DifferentiableOn ℂ F {z | 0 < z.im})
    (hi : InjOn F {z | 0 < z.im}) {a : ℂ}
    (ha : ∀ z, 0 < z.im → F z ≠ a) {r t₀ : ℝ} {β : ℝ → ℂ}
    (hr : 0 < r) (ht₀ : 0 < t₀) (hβ : ContinuousOn β (Icc 0 t₀)) (hβ₀ : β 0 = 0)
    (hβH : ∀ t ∈ Ioc 0 t₀, 0 < (β t).im)
    (hsmall : ∀ t ∈ Ioc 0 t₀, ‖F (β t) - a‖ ≤ r * Real.exp (-65536)) :
    ∀ δ : ℝ, 0 < δ → ∃ B ∈ Ioo 0 δ,
      (∀ θ ∈ Ioo 0 Real.pi,
        ‖F ((B : ℂ) * Complex.exp ((θ : ℂ) * Complex.I)) - a‖ < r / 4) ∧
      ∀ z : ℂ, B / 8 ≤ ‖z‖ → ‖z‖ ≤ B → ‖z‖ / 2 ≤ z.im → ‖F z - a‖ < r / 4 := by
…

theorem OAI.SLEExactGauge.SmallImageSemicircle.access_guide_has_arbitrarily_small_quarter_image_sector line 187

Source documentation

Full access-guide formulation: convergence to the omitted boundary value itself supplies the initial short segment needed above.

theorem access_guide_has_arbitrarily_small_quarter_image_sector
    {F : ℂ → ℂ} (hF : DifferentiableOn ℂ F {z | 0 < z.im})
    (hi : InjOn F {z | 0 < z.im}) {a : ℂ}
    (ha : ∀ z, 0 < z.im → F z ≠ a) {r T : ℝ} {β : ℝ → ℂ}
    (hr : 0 < r) (hT : 0 < T) (hβ : ContinuousOn β (Icc 0 T)) (hβ₀ : β 0 = 0)
    (hβH : ∀ t ∈ Ioc 0 T, 0 < (β t).im)
    (hlimit : Tendsto (F ∘ β) (𝓝[>] 0) (𝓝 a)) :
    ∀ δ : ℝ, 0 < δ → ∃ B ∈ Ioo 0 δ,
      (∀ θ ∈ Ioo 0 Real.pi,
        ‖F ((B : ℂ) * Complex.exp ((θ : ℂ) * Complex.I)) - a‖ < r / 4) ∧
      ∀ z : ℂ, B / 8 ≤ ‖z‖ → ‖z‖ ≤ B → ‖z‖ / 2 ≤ z.im → ‖F z - a‖ < r / 4 := by
…