MultipointGeometry.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Geometric decay of the multipoint interaction follows from the univalent disk growth inequality in Duren, Univalent Functions (1983), Section 2.3.

def OAI.SLEExactGauge.PublishedDiskUnivalentGrowth line 14
lemma OAI.SLEExactGauge.Multipoint.neg_log_sq_le_radius_ratio line 23
Source documentation
The hyperbolic interaction is bounded by the square root of the ratio of conformal radius to point separation.
```
lemma neg_log_sq_le_radius_ratio {ρ R D : ℝ}
    (hρ : 0 < ρ) (hρ1 : ρ < 1) (hD : 0 < D)
    (hgrowth : D ≤ R*ρ/(1-ρ)^2) : (-Real.log ρ)^2 ≤ R/D := by
…
```
lemma OAI.SLEExactGauge.Multipoint.interaction_decay_of_growth line 60

theorem OAI.SLEExactGauge.Multipoint.disk_interaction_decay line 79

Source documentation

A physical disk uniformization supplies the growth hypothesis used above. No derivative of the original half-plane map is bounded.

theorem disk_interaction_decay (hgrowth : PublishedDiskUnivalentGrowth)
    (f : ℂ → ℂ) (hf : DifferentiableOn ℂ f (ball 0 1))
    (hinj : InjOn f (ball 0 1)) (z : ℂ) (hz : z ∈ ball (0 : ℂ) 1)
    (hz0 : z ≠ 0) (b a u : ℝ) (hb : b ≤ ‖f z-f 0‖)
    (hradius : ‖deriv f 0‖ = b*Real.exp (-2*a*u)) :
    -Real.log ‖z‖ ≤ Real.exp (-a*u) := by
…

Mentions: OAI.SLEExactGauge.PublishedDiskUnivalentGrowth

lemma OAI.SLEExactGauge.Multipoint.interaction_decay_max line 93