ScaleTraceLaw.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Equality of actual continuous SLE trace laws under capacity scaling. The Brownian driver laws agree by finite-dimensional uniqueness. Canonical reverse-flow approximants transfer the measurable trace factor through that law equality, so no scaling law for geometric events is assumed.

theorem OAI.SLEExactGauge.ScaleTraceLaw.brownian_continuous_path_law line 24

theorem OAI.SLEExactGauge.ScaleTraceLaw.trace_path_law_of_driver_law line 53

Source documentation

Equality of continuous driver laws gives equality of the actual trace laws. Reverse-flow approximants identify the trace factor on the common law.

theorem trace_path_law_of_driver_law
    {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (B B' : ℝ≥0 → Ω → ℝ) (hB : IsBrownianReal B P)
    (hm : ∀ t, Measurable (B t)) (hm' : ∀ t, Measurable (B' t))
    (hc : ∀ ω, Continuous (fun t => B t ω)) (hc' : ∀ ω, Continuous (fun t => B' t ω))
    (γ γ' : Ω → ℝ≥0 → ℂ) (G F G' F' : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B t ω) (γ ω) (G ω) (F ω))
    (hw' : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B' t ω) (γ' ω) (G' ω) (F' ω))
    (hlaw : P.map (sourceDriverPath B hc) = P.map (sourceDriverPath B' hc')) :
    P.map (sourceTracePath γ (fun ω => (hw ω).1)) =
      P.map (sourceTracePath γ' (fun ω => (hw' ω).1)) := by
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.sourceDriverPath, OAI.SLEExactGauge.sourceTracePath

def OAI.SLEExactGauge.ScaleTraceLaw.scalePath line 123
Source documentation
The actual capacity-normalized scaling on continuous trace paths.
```
def scalePath (c : ℝ≥0) (p : C(ℝ≥0, ℂ)) : C(ℝ≥0, ℂ) :=
…
```
theorem OAI.SLEExactGauge.ScaleTraceLaw.measurable_scalePath line 127

theorem OAI.SLEExactGauge.ScaleTraceLaw.scaled_trace_path_law line 132

Source documentation

The scaled actual capacity trace has exactly the original path law.

theorem scaled_trace_path_law
    {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (B : ℝ≥0 → Ω → ℝ) (hB : IsBrownianReal B P)
    (hm : ∀ t, Measurable (B t)) (hc : ∀ ω, Continuous (fun t => B t ω))
    (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B t ω) (γ ω) (G ω) (F ω))
    (c : ℝ≥0) (hcpos : 0 < c) :
    P.map (fun ω => scalePath c (sourceTracePath γ (fun ω => (hw ω).1) ω)) =
      P.map (sourceTracePath γ (fun ω => (hw ω).1)) := by
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.ScaleTraceLaw.scalePath, OAI.SLEExactGauge.sourceTracePath