BoundaryScaleLaw.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Finite boundary charts commute with normalization. Capacity scaling changes only the clock of the physical image path, and therefore preserves the first-front success-and-sausage event.

theorem OAI.SLEExactGauge.BoundaryScaleLaw.finite_boundary_ext line 22
def OAI.SLEExactGauge.BoundaryScaleLaw.scaleClosed line 44
theorem OAI.SLEExactGauge.BoundaryScaleLaw.normalized_boundary_eq line 51
def OAI.SLEExactGauge.BoundaryScaleLaw.clockPath line 67
theorem OAI.SLEExactGauge.BoundaryScaleLaw.measurable_clockPath line 70
theorem OAI.SLEExactGauge.BoundaryScaleLaw.boundary_scale_clock_identity line 76

theorem OAI.SLEExactGauge.BoundaryScaleLaw.boundary_scale_path_law line 101

Source documentation

The normalized physical path has the same law as a deterministic capacity-clock change of the unnormalized physical path.

theorem boundary_scale_path_law
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (p : Ω → C(ℝ≥0, ℂ)) (hp : Measurable p)
    (hclosed : ∀ᵐ ω ∂P, ClosedPathProperty (p ω))
    (c : ℝ≥0) (hc : 0 < c) (f : C(closedHalfPlane, ℂ))
    (hlaw : P.map (fun ω => ScaleTraceLaw.scalePath c (p ω)) = P.map p) :
    P.map (fun ω => finiteBoundaryPath (f.comp (scaleClosed c)) (p ω)) =
      P.map (fun ω => clockPath (OrderIso.mulLeft₀ (c ^ 2) (pow_pos hc 2))
        (finiteBoundaryPath f (p ω))) := by
…

Mentions: OAI.SLEExactGauge.ClosedPathProperty, OAI.SLEExactGauge.closedHalfPlane, OAI.SLEExactGauge.ScaleTraceLaw.scalePath, OAI.SLEExactGauge.finiteBoundaryPath, OAI.SLEExactGauge.BoundaryScaleLaw.scaleClosed, OAI.SLEExactGauge.BoundaryScaleLaw.clockPath

def OAI.SLEExactGauge.BoundaryScaleLaw.frontMassEvent line 126
theorem OAI.SLEExactGauge.BoundaryScaleLaw.measurableSet_frontMassEvent line 133
theorem OAI.SLEExactGauge.BoundaryScaleLaw.mem_frontMassEvent_clock line 150

theorem OAI.SLEExactGauge.BoundaryScaleLaw.frontMassEvent_boundary_scale_probability line 164

Source documentation

Normalize the inverse chart without changing the physical first-front event probability. The scale law is the actual SLE path law.

theorem frontMassEvent_boundary_scale_probability
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (γ : Ω → C(ℝ≥0, ℂ)) (hγ : Measurable γ)
    (hclosed : ∀ᵐ ω ∂P, ClosedPathProperty (γ ω))
    (ell : ℝ≥0) (hell : 0 < ell) (f : C(closedHalfPlane, ℂ))
    (hlaw : P.map (fun ω => ScaleTraceLaw.scalePath ell (γ ω)) = P.map γ)
    (p : ℂ → ℝ) (V : Set ℂ) (a : ℂ) (ε κ v c : ℝ) (R K : Set ℂ)
    (hK : IsClosed K) (hp : ContinuousOn p K) (hV : IsOpen V) (hVK : V ⊆ K) :
    P {ω | finiteBoundaryPath (f.comp (scaleClosed ell)) (γ ω) ∈ frontMassEvent p V a ε κ v c R} =
      P {ω | finiteBoundaryPath f (γ ω) ∈ frontMassEvent p V a ε κ v c R} := by
…