MultipointLogClockTransport.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The smooth logarithmic-coordinate factors use precisely the source radius clock. These identities transport the proved one-point and pair costs to the normalized branches, in capacity-two physical time.

lemma OAI.SLEExactGauge.Multipoint.logFactorClock_eq_logRadiusClock line 17
lemma OAI.SLEExactGauge.Multipoint.regulator_scaled_argument line 22
lemma OAI.SLEExactGauge.Multipoint.logVelocity_logCoordinates line 28
lemma OAI.SLEExactGauge.Multipoint.logFactor_single_integrand_nonneg line 40
lemma OAI.SLEExactGauge.Multipoint.logFactor_pair_integrand_nonneg line 48
lemma OAI.SLEExactGauge.IsCapacityTwoWitness.logFactorClock_sub line 65

theorem OAI.SLEExactGauge.IsCapacityTwoWitness.logFactor_single_regulator_integral_le line 84

Source documentation

The one-point regulator cost in the smooth factor's clock units.

theorem IsCapacityTwoWitness.logFactor_single_regulator_integral_le
    {κ : ℝ} (hκ : 0 < κ) {B : ℝ≥0 → ℝ} (hB : Continuous B)
    {γ : ℝ≥0 → ℂ} {G F : ℝ≥0 → ℂ → ℂ}
    (hw : IsCapacityTwoWitness (fun t => Real.sqrt κ*B t) γ G F)
    (σ T : ℝ≥0) (hσT : σ ≤ T) (z : ℂ) (hz : z ∈ survivingDomain γ T)
    {β target : ℝ} (hβ : 0 < β) (htarget : 0 ≤ target)
    (hclock : Multipoint.logFactorClock κ (logLoewnerCoordinates G z T) -
      Multipoint.logFactorClock κ (logLoewnerCoordinates G z σ) ≤ target) :
    (∫ t in (σ : ℝ)..(T : ℝ),
      Multipoint.regulator β target
        (Multipoint.logFactorClock κ (logLoewnerCoordinates G z t) -
          Multipoint.logFactorClock κ (logLoewnerCoordinates G z σ)) *
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.survivingDomain, OAI.SLEExactGauge.Multipoint.logFactorClock, OAI.SLEExactGauge.logLoewnerCoordinates, OAI.SLEExactGauge.Multipoint.regulator

theorem OAI.SLEExactGauge.IsCapacityTwoWitness.logFactor_single_discount_le line 119

Source documentation

Including the generator's factor κ gives exactly the source bound.

theorem IsCapacityTwoWitness.logFactor_single_discount_le
    {κ : ℝ} (hκ : 0 < κ) {B : ℝ≥0 → ℝ} (hB : Continuous B)
    {γ : ℝ≥0 → ℂ} {G F : ℝ≥0 → ℂ → ℂ}
    (hw : IsCapacityTwoWitness (fun t => Real.sqrt κ*B t) γ G F)
    (σ T : ℝ≥0) (hσT : σ ≤ T) (z : ℂ) (hz : z ∈ survivingDomain γ T)
    {β target : ℝ} (hβ : 0 < β) (htarget : 0 ≤ target)
    (hclock : Multipoint.logFactorClock κ (logLoewnerCoordinates G z T) -
      Multipoint.logFactorClock κ (logLoewnerCoordinates G z σ) ≤ target) :
    κ*(∫ t in (σ : ℝ)..(T : ℝ),
      Multipoint.regulator β target
        (Multipoint.logFactorClock κ (logLoewnerCoordinates G z t) -
          Multipoint.logFactorClock κ (logLoewnerCoordinates G z σ)) *
…

theorem OAI.SLEExactGauge.IsCapacityTwoWitness.logFactor_pair_regulator_integral_le line 140

Source documentation

Pair interaction cost for the source-normalized regulator branches. The physical-time interaction budget remains in capacity-two units.

theorem IsCapacityTwoWitness.logFactor_pair_regulator_integral_le
    {κ : ℝ} (hκ : 0 < κ) {B : ℝ≥0 → ℝ} (hB : Continuous B)
    {γ : ℝ≥0 → ℂ} {G F : ℝ≥0 → ℂ → ℂ}
    (hw : IsCapacityTwoWitness (fun t => Real.sqrt κ*B t) γ G F)
    (hgrowth : PublishedDiskUnivalentGrowth)
    (J : ℂ → ℂ) (hJ : DifferentiableOn ℂ J upperHalfPlane)
    (hJinj : InjOn J upperHalfPlane)
    (σz σw s T : ℝ≥0) (hσz : σz ≤ s) (hσw : σw ≤ s) (hsT : s ≤ T)
    (z w : ℂ) (hz : z ∈ survivingDomain γ T) (hw' : w ∈ survivingDomain γ T)
    (hne : z ≠ w)
    (hbz : physicalConformalRadius J G σz z ≤ dist (J z) (J w))
    (hbw : physicalConformalRadius J G σw w ≤ dist (J z) (J w))
…

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

lemma OAI.SLEExactGauge.IsCapacityTwoWitness.logFactorClock_sub_continuousOn line 188
lemma OAI.SLEExactGauge.IsCapacityTwoWitness.logVelocity_continuousOn line 201

theorem OAI.SLEExactGauge.IsCapacityTwoWitness.logFactor_single_intervalIntegrable line 216

Source documentation

Integrability for the exact source-clock single-point cost on its own active interval. The endpoint may be specific to this marked point.

theorem IsCapacityTwoWitness.logFactor_single_intervalIntegrable
    {κ : ℝ} {B : ℝ≥0 → ℝ} (hB : Continuous B)
    {γ : ℝ≥0 → ℂ} {G F : ℝ≥0 → ℂ → ℂ}
    (hw : IsCapacityTwoWitness (fun t => Real.sqrt κ*B t) γ G F)
    (σ T : ℝ≥0) (hσT : σ ≤ T) (z : ℂ) (hz : z ∈ survivingDomain γ T)
    (β target : ℝ) :
    IntervalIntegrable (fun t : ℝ =>
      Multipoint.regulator β target
        (Multipoint.logFactorClock κ (logLoewnerCoordinates G z t) -
          Multipoint.logFactorClock κ (logLoewnerCoordinates G z σ)) *
        Multipoint.logVelocity κ (logLoewnerCoordinates G z t) (B t.toNNReal)^2)
      volume (σ : ℝ) (T : ℝ) := by
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.survivingDomain, OAI.SLEExactGauge.Multipoint.regulator, OAI.SLEExactGauge.Multipoint.logFactorClock, OAI.SLEExactGauge.logLoewnerCoordinates, OAI.SLEExactGauge.Multipoint.logVelocity

theorem OAI.SLEExactGauge.IsCapacityTwoWitness.logFactor_pair_intervalIntegrable line 240

Source documentation

Integrability for the exact source-clock pair cost on the overlap of the two active intervals; the common endpoint may be their minimum.

theorem IsCapacityTwoWitness.logFactor_pair_intervalIntegrable
    {κ : ℝ} {B : ℝ≥0 → ℝ} (hB : Continuous B)
    {γ : ℝ≥0 → ℂ} {G F : ℝ≥0 → ℂ → ℂ}
    (hw : IsCapacityTwoWitness (fun t => Real.sqrt κ*B t) γ G F)
    (σz σw s T : ℝ≥0) (hσz : σz ≤ s) (hσw : σw ≤ s) (hsT : s ≤ T)
    (z w : ℂ) (hz : z ∈ survivingDomain γ T) (hw' : w ∈ survivingDomain γ T)
    (β M Uz Uw : ℝ) :
    IntervalIntegrable (fun t : ℝ =>
      (Multipoint.regulator β Uz
        (Multipoint.logFactorClock κ (logLoewnerCoordinates G z t) -
          Multipoint.logFactorClock κ (logLoewnerCoordinates G z σz)) *
       Multipoint.regulator β Uw
…