SmallImageSemicircle.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Angular Sobolev estimates for the small-image semicircle lemma es:good-semicircle. In particular, the absolute continuity used below is proved for the actual clipped conformal logarithm.

lemma OAI.SLEExactGauge.SmallImageSemicircle.integral_abs_le_angular_energy line 17

theorem OAI.SLEExactGauge.SmallImageSemicircle.angular_oscillation_bound line 33

Source documentation

A section which is absolutely continuous on compact subintervals has oscillation controlled by its full angular derivative energy.

theorem angular_oscillation_bound {f : ℝ → ℝ} {x y : ℝ}
    (hx : x ∈ Ioo 0 Real.pi) (hy : y ∈ Ioo 0 Real.pi)
    (hf : AbsolutelyContinuousOnInterval f x y)
    (hderiv : MemLp (deriv f) 2 (volume.restrict (Ioo 0 Real.pi))) :
    |f y - f x| ≤ Real.sqrt Real.pi *
      Real.sqrt (∫ θ in Ioo 0 Real.pi, (deriv f θ) ^ 2) := by
…

theorem OAI.SLEExactGauge.SmallImageSemicircle.anchored_angular_bound line 56

theorem OAI.SLEExactGauge.SmallImageSemicircle.anchored_angular_bound_of_energy line 66

Source documentation

The exact angular constant in the manuscript.

theorem anchored_angular_bound_of_energy {f : ℝ → ℝ} {θ₀ H : ℝ}
    (hH : 0 ≤ H) (hθ₀ : θ₀ ∈ Ioo 0 Real.pi) (hzero : f θ₀ = 0)
    (hac : ∀ θ ∈ Ioo 0 Real.pi, AbsolutelyContinuousOnInterval f θ₀ θ)
    (hderiv : MemLp (deriv f) 2 (volume.restrict (Ioo 0 Real.pi)))
    (henergy : (∫ φ in Ioo 0 Real.pi, (deriv f φ) ^ 2) ≤ 2 * Real.pi * H) :
    ∀ θ ∈ Ioo 0 Real.pi, f θ ≤ Real.pi * Real.sqrt (2 * H) := by
…

def OAI.SLEExactGauge.SmallImageSemicircle.stripPoint line 85
lemma OAI.SLEExactGauge.SmallImageSemicircle.stripPoint_mem line 87

theorem OAI.SLEExactGauge.SmallImageSemicircle.conformal_section_absolutelyContinuous line 95

Source documentation

Compact angular sections of the actual conformal logarithm are absolutely continuous. The omitted point removes the logarithmic singularity.

theorem conformal_section_absolutelyContinuous
    {F : ℂ → ℂ} (hF : DifferentiableOn ℂ F {z | 0 < z.im})
    {a : ℂ} (ha : ∀ z, 0 < z.im → F z ≠ a)
    {r : ℝ} (hr : 0 < r) (H v : ℝ) {x y : ℝ}
    (hx : x ∈ Ioo 0 Real.pi) (hy : y ∈ Ioo 0 Real.pi) :
    AbsolutelyContinuousOnInterval
      (fun θ => conformalStripLog F a r H (stripPoint v θ)) x y := by
…

Mentions: OAI.SLEExactGauge.conformalStripLog, OAI.SLEExactGauge.SmallImageSemicircle.stripPoint

lemma OAI.SLEExactGauge.SmallImageSemicircle.angular_deriv_le_gradient line 121

theorem OAI.SLEExactGauge.SmallImageSemicircle.exists_section_of_strip_energy line 135

Source documentation

A unit logarithmic slab contains a section whose full angular energy is at most the total strip energy. Differentiability is required only almost everywhere, as supplied by the locally Lipschitz conformal logarithm.

theorem exists_section_of_strip_energy
    (u : ℂ → ℝ) (q : ℝ)
    (hg : MemLp (gradient u) 2
      (volume.restrict {z : ℂ | 0 < z.im ∧ z.im < Real.pi}))
    (hd : ∀ᵐ z ∂volume, z ∈ {z : ℂ | 0 < z.im ∧ z.im < Real.pi} →
      DifferentiableAt ℝ u z) :
    ∃ v ∈ Ioo q (q + 1),
      MemLp (deriv (fun θ => u (stripPoint v θ))) 2 (volume.restrict (Ioo 0 Real.pi)) ∧
      (∫ θ in Ioo 0 Real.pi, (deriv (fun t => u (stripPoint v t)) θ) ^ 2) ≤
        ∫ z in {z : ℂ | 0 < z.im ∧ z.im < Real.pi}, ‖gradient u z‖ ^ 2 := by
…

Mentions: OAI.SLEExactGauge.SmallImageSemicircle.stripPoint

theorem OAI.SLEExactGauge.SmallImageSemicircle.access_segment_section_anchor line 223

Source documentation

The guide crosses every smaller semicircle, supplying the anchor required by the angular Sobolev estimate.

theorem access_segment_section_anchor
    {F : ℂ → ℂ} {a : ℂ} {r t₀ : ℝ} {β : ℝ → ℂ}
    (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)
    {v : ℝ} (hv : v < Real.log ‖β t₀‖) :
    ∃ θ ∈ Ioo 0 Real.pi, ‖F (Complex.exp (stripPoint v θ)) - a‖ ≤ r := by
…

Mentions: OAI.SLEExactGauge.SmallImageSemicircle.stripPoint

theorem OAI.SLEExactGauge.SmallImageSemicircle.exists_small_image_semicircle_of_anchors line 260

Source documentation

The exact semicircle estimate before writing the base radius as r * exp (-A). The section anchor is a direct consequence of an access guide, as proved above.

theorem exists_small_image_semicircle_of_anchors
    {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 q : ℝ}
    (hr : 0 < r) (hA : 2 * Real.pi ^ 2 < A)
    (hanchor : ∀ v ∈ Ioo q (q + 1),
      ∃ θ ∈ Ioo 0 Real.pi, ‖F (Complex.exp (stripPoint v θ)) - a‖ ≤ r) :
    ∃ B ∈ Ioo (Real.exp q) (Real.exp (q + 1)),
      ∀ θ ∈ Ioo 0 Real.pi,
        ‖F ((B : ℂ) * Complex.exp ((θ : ℂ) * Complex.I)) - a‖ ≤
          r * Real.exp (Real.pi * Real.sqrt (2 * A)) := by
…

Mentions: OAI.SLEExactGauge.SmallImageSemicircle.stripPoint

theorem OAI.SLEExactGauge.SmallImageSemicircle.exists_small_image_semicircle line 318

Source documentation

es:good-semicircle, with the initial short guide segment appearing explicitly. This proves the manuscript's bound in every unit logarithmic slab below the segment's terminal radius.

theorem exists_small_image_semicircle
    {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 q 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))
    (hq : q + 1 ≤ Real.log ‖β t₀‖) :
    ∃ B ∈ Ioo (Real.exp q) (Real.exp (q + 1)),
      ∀ θ ∈ Ioo 0 Real.pi,
        ‖F ((B : ℂ) * Complex.exp ((θ : ℂ) * Complex.I)) - a‖ ≤
…

lemma OAI.SLEExactGauge.SmallImageSemicircle.semicircle_exponential_lt_quarter line 339
Source documentation
The numerical choice used after the semicircle and sector estimates.
```
lemma semicircle_exponential_lt_quarter {A : ℝ} (hA : 64 ≤ A) :
    Real.exp (-A + Real.pi * Real.sqrt (2 * A) + 6) < 1 / 4 := by
…
```

theorem OAI.SLEExactGauge.SmallImageSemicircle.exists_arbitrarily_small_image_semicircle line 362

Source documentation

The guide supplies small-image semicircles at arbitrarily small radii. The image estimate is uniform in the chosen radius.

theorem exists_arbitrarily_small_image_semicircle
    {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)) := by
…