MultipointPhysicalBudget.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual physical-domain interaction budget. This statement uses capacity-two time throughout: the radius clocks satisfy R = b exp(-4u), and the Green derivative has coefficient four. No bound on the derivative of the original conformal map is assumed.

theorem OAI.SLEExactGauge.IsCapacityTwoWitness.physical_interaction_decay_of_radius_le line 19

Source documentation

A conformal-radius upper bound suffices for geometric interaction decay; the physical clock need not be specified by equality.

theorem IsCapacityTwoWitness.physical_interaction_decay_of_radius_le
    {U : ℝ≥0 → ℝ} {γ : ℝ≥0 → ℂ} {G F : ℝ≥0 → ℂ → ℂ}
    (hw : IsCapacityTwoWitness U γ G F) (hgrowth : PublishedDiskUnivalentGrowth)
    (J : ℂ → ℂ) (hJ : DifferentiableOn ℂ J upperHalfPlane)
    (hJinj : InjOn J upperHalfPlane)
    (t : ℝ≥0) (z w : ℂ) (hz : z ∈ survivingDomain γ t)
    (hw' : w ∈ survivingDomain γ t) (hne : z ≠ w)
    (b a u : ℝ) (hb : b ≤ dist (J z) (J w))
    (hR : physicalConformalRadius J G t z ≤ b * Real.exp (-2 * a * u)) :
    halfPlaneGreen (G t z) (G t w) ≤ Real.exp (-a * u) := by
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.PublishedDiskUnivalentGrowth, OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.survivingDomain, OAI.SLEExactGauge.physicalConformalRadius, OAI.SLEExactGauge.halfPlaneGreen

lemma OAI.SLEExactGauge.halfPlaneGreen_symm line 36

theorem OAI.SLEExactGauge.IsCapacityTwoWitness.physical_pair_interaction_budget line 50

Source documentation

Both radius caps yield the decay in the maximum of the two clocks; the proved Green drop then pays for every weighted interaction shell.

theorem IsCapacityTwoWitness.physical_pair_interaction_budget
    {U : ℝ≥0 → ℝ} {γ : ℝ≥0 → ℂ} {G F : ℝ≥0 → ℂ → ℂ}
    (hw : IsCapacityTwoWitness U γ G F) (hU : Continuous U)
    (hgrowth : PublishedDiskUnivalentGrowth)
    (J : ℂ → ℂ) (hJ : DifferentiableOn ℂ J upperHalfPlane)
    (hJinj : InjOn J upperHalfPlane)
    (s T : ℝ≥0) (hsT : s ≤ T) (z w : ℂ)
    (hz : z ∈ survivingDomain γ T) (hw' : w ∈ survivingDomain γ T) (hne : z ≠ w)
    (bz bw : ℝ) (hbz : bz ≤ dist (J z) (J w)) (hbw : bw ≤ dist (J z) (J w))
    {c : ℝ} (hc : 0 ≤ c) (hca : 2 * c < 2) (u v : ℝ → ℝ)
    (hu : ContinuousOn u (Icc (s : ℝ) (T : ℝ)))
    (hv : ContinuousOn v (Icc (s : ℝ) (T : ℝ)))
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.PublishedDiskUnivalentGrowth, OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.survivingDomain