OAI/Probability/SLE/Multipoint/MultipointInteractionShells.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The Green drop bounds the mass of every clock shell. The first point of the closed clock tail gives the bound even when a clock is constant on an interval. Disjoint measurable shells then give the manuscript's weighted interaction budget.

  1. def OAI.SLEExactGauge.Multipoint.clockTail line 17
  2. def OAI.SLEExactGauge.Multipoint.clockShell line 20
  3. lemma OAI.SLEExactGauge.Multipoint.clockTail_isClosed line 23
  4. lemma OAI.SLEExactGauge.Multipoint.clockTail_isCompact line 27
  5. lemma OAI.SLEExactGauge.Multipoint.clockShell_measurableSet line 31
  6. lemma OAI.SLEExactGauge.Multipoint.mem_clockShell line 36
  7. lemma OAI.SLEExactGauge.Multipoint.clockShell_pairwise line 46
  8. lemma OAI.SLEExactGauge.Multipoint.iUnion_clockShell line 59
  9. theorem OAI.SLEExactGauge.Multipoint.interaction_shell_mass_bound line 73

    Source documentation

    A future Green-drop bound and the exponential interaction decay give the exact mass bound for a single shell of the increasing clock.

    theorem interaction_shell_mass_bound
    {s T a M : ℝ} (ha : 0 < a) (hM : 0 ≤ M) (q R L : ℝ → ℝ)
    (hq : ContinuousOn q (Icc s T)) (hR : ContinuousOn R (Icc s T))
    (hR0 : ∀ t ∈ Icc s T, 0 ≤ R t)
    (hdrop : ∀ t ∈ Icc s T, (∫ v in t..T, R v) ≤ L t / (2 * a))
    (hdecay : ∀ t ∈ Icc s T, L t ≤ M * Real.exp (-a * q t)) (k : ℕ) :
    (∫ t in clockShell s T q k, R t) ≤ M * Real.exp (-a * k) / (2 * a) := by
…

    Mentions: OAI.SLEExactGauge.Multipoint.q, OAI.SLEExactGauge.Multipoint.clockShell

  10. lemma OAI.SLEExactGauge.Multipoint.weighted_shell_sum_le_prefactor line 112
  11. theorem OAI.SLEExactGauge.Multipoint.weighted_interaction_integral_le line 134

    Source documentation

    The full weighted interaction bound, derived from the Green drop; no shell-mass estimate is assumed.

    theorem weighted_interaction_integral_le
    {s T a c M : ℝ} (hsT : s ≤ T) (ha : 0 < a) (hM : 0 ≤ M)
    (hc : 0 ≤ c) (hca : 2 * c < a)
    (u v R L : ℝ → ℝ)
    (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)
    (hR : ContinuousOn R (Icc s T)) (hR0 : ∀ t ∈ Icc s T, 0 ≤ R t)
    (hdrop : ∀ t ∈ Icc s T, (∫ x in t..T, R x) ≤ L t / (2 * a))
    (hdecay : ∀ t ∈ Icc s T, L t ≤ M * Real.exp (-a * max (u t) (v t))) :
    (∫ t in s..T, Real.exp (c * (u t + v t)) * R t) ≤ M * interactionBudget a c := by
…

    Mentions: OAI.SLEExactGauge.Multipoint.interactionBudget

  12. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.weighted_interaction_integral_le line 199

    Source documentation

    The weighted-shell estimate for the actual capacity-two Loewner maps. The pair drop is supplied by the proved Green-kernel identity. Its sole remaining geometric premise is the interaction decay during joint activity.

    theorem IsCapacityTwoWitness.weighted_interaction_integral_le
    {U : ℝ≥0 → ℝ} {γ : ℝ≥0 → ℂ} {G F : ℝ≥0 → ℂ → ℂ}
    (hw : IsCapacityTwoWitness U γ G F) (hU : Continuous U)
    (s T : ℝ≥0) (hsT : s ≤ T) (z w : ℂ)
    (hz : z ∈ survivingDomain γ T) (hw' : w ∈ survivingDomain γ T) (hne : z ≠ w)
    {c M : ℝ} (hM : 0 ≤ M) (hc : 0 ≤ c) (hca : 2 * c < 2) (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 : ℝ),
      halfPlaneGreen (G t.toNNReal z) (G t.toNNReal w) ≤
…

    Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.survivingDomain, OAI.SLEExactGauge.halfPlaneGreen