MultipointLoewnerDrop.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The source time normalization of the pair-interaction drop. The two uncentered Loewner paths have velocity a/(f-U), while the common real driver is only assumed continuous. No derivative of Brownian motion is used.

def OAI.SLEExactGauge.Multipoint.loewnerPoissonRate line 16
lemma OAI.SLEExactGauge.Multipoint.loewnerPoissonRate_continuousOn line 19
lemma OAI.SLEExactGauge.Multipoint.loewnerPoissonRate_nonneg line 35

theorem OAI.SLEExactGauge.Multipoint.loewner_interaction_drop line 41

Source documentation

Exact fundamental-theorem-of-calculus form of the interaction identity in the manuscript's time normalization.

theorem loewner_interaction_drop
    {s T a : ℝ} (hs : 0 ≤ s) (hsT : s ≤ T)
    (f g : ℝ → ℂ) (U : ℝ → ℝ) (hU : ContinuousOn U (Icc s T))
    (hf : ∀ t ∈ Icc s T, HasDerivWithinAt f ((a : ℂ) / (f t - (U t : ℂ))) (Ici 0) t)
    (hg : ∀ t ∈ Icc s T, HasDerivWithinAt g ((a : ℂ) / (g t - (U t : ℂ))) (Ici 0) t)
    (hfi : ∀ t ∈ Icc s T, 0 < (f t).im)
    (hgi : ∀ t ∈ Icc s T, 0 < (g t).im)
    (hne : ∀ t ∈ Icc s T, f t ≠ g t) :
    2 * a * (∫ t in s..T, loewnerPoissonRate f U t * loewnerPoissonRate g U t) =
      interaction (f s) (g s) - interaction (f T) (g T) := by
…

Mentions: OAI.SLEExactGauge.Multipoint.loewnerPoissonRate, OAI.SLEExactGauge.Multipoint.interaction

theorem OAI.SLEExactGauge.Multipoint.loewner_interaction_future_bound line 76

theorem OAI.SLEExactGauge.Multipoint.loewner_weighted_interaction_integral_le line 94

Source documentation

Source-normalized weighted interaction, with the interval drop discharged from the actual Loewner ODE. Only the geometric decay remains as a separate premise.

theorem loewner_weighted_interaction_integral_le
    {s T a c M : ℝ} (hs : 0 ≤ s) (hsT : s ≤ T) (ha : 0 < a)
    (hM : 0 ≤ M) (hc : 0 ≤ c) (hca : 2 * c < a)
    (f g : ℝ → ℂ) (U : ℝ → ℝ) (hU : ContinuousOn U (Icc s T))
    (hf : ∀ t ∈ Icc s T, HasDerivWithinAt f ((a : ℂ) / (f t - (U t : ℂ))) (Ici 0) t)
    (hg : ∀ t ∈ Icc s T, HasDerivWithinAt g ((a : ℂ) / (g t - (U t : ℂ))) (Ici 0) t)
    (hfi : ∀ t ∈ Icc s T, 0 < (f t).im)
    (hgi : ∀ t ∈ Icc s T, 0 < (g t).im)
    (hne : ∀ t ∈ Icc s T, f t ≠ g t)
    (u v : ℝ → ℝ) (hu : ContinuousOn u (Icc s T)) (hv : ContinuousOn v (Icc s T))
    (hu0 : ∀ t ∈ Icc s T, 0 ≤ u t) (hv0 : ∀ t ∈ Icc s T, 0 ≤ v t)
    (hdecay : ∀ t ∈ Icc s T, interaction (f t) (g t) ≤
…

Mentions: OAI.SLEExactGauge.Multipoint.interaction