OAI/Probability/SLE/Geometry/SpatialPastKernels.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Spatial Loewner kernels up to a deterministic time depend only on the driver up to that time. The marked point is kept as a measurable parameter.

  1. lemma OAI.SLEExactGauge.clipped_flow_eqOn_prefix line 15
  2. lemma OAI.SLEExactGauge.spatial_clipped_eqOn_prefix line 44
  3. lemma OAI.SLEExactGauge.exists_past_spatial_family line 57
  4. theorem OAI.SLEExactGauge.actual_spatial_past_kernels line 87

    Source documentation

    All three spatial kernels are jointly measurable in the marked point, sample, and time restricted to the natural past at T.

    theorem actual_spatial_past_kernels
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {B : ℝ≥0 → Ω → ℝ}
    (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 ω)) (T : ℝ≥0) :
    let mT := Filtration.natural B (fun t => (hm t).stronglyMeasurable) T
…

    Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness