OAI/Probability/SLE/Mass/LevelApproximationKernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The conditional Green kernel of the part of a level measure still to come. The level hit is represented by an actual Brownian stopping time; no measurability of a geometrically defined filtration is assumed.

  1. def OAI.SLEExactGauge.Multipoint.levelRemainderGreen line 16
  2. def OAI.SLEExactGauge.Multipoint.levelCurrentGreen line 22
  3. lemma OAI.SLEExactGauge.Multipoint.levelRemainderGreen_nonneg line 28
  4. lemma OAI.SLEExactGauge.Multipoint.levelCurrentGreen_nonneg line 38
  5. lemma OAI.SLEExactGauge.Multipoint.actual_greenDensity_joint_measurable line 48
  6. lemma OAI.SLEExactGauge.Multipoint.levelRemainderGreen_joint_measurable line 67
  7. lemma OAI.SLEExactGauge.Multipoint.levelCurrentGreen_joint_measurable line 78
  8. theorem OAI.SLEExactGauge.Multipoint.levelRemainderGreen_condExp line 90
  9. theorem OAI.SLEExactGauge.Multipoint.levelRemainderGreen_setIntegral line 147
  10. theorem OAI.SLEExactGauge.Multipoint.levelRemainderGreen_setLIntegral line 171
  11. theorem OAI.SLEExactGauge.Multipoint.levelRemainderGreen_spatial_kernel line 197

    Source documentation

    The finite-level kernel identity against every nonnegative spatial test, on every event known at time t.

    theorem levelRemainderGreen_spatial_kernel
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (hBm : Measurable (Function.uncurry B))
    (hBc : ∀ ω, Continuous (fun t => B t ω)) (hB0 : ∀ ω, B 0 ω = 0)
    {κ : ℝ} (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ ω, IsCapacityTwoWitness
      (fun s => Real.sqrt κ * B s ω) (γ ω) (G ω) (F ω))
    (u : ℝ) (hu : 0 ≤ u) (t : ℝ≥0) (K : Set ℂ)
    (hK : MeasurableSet K) (hKH : K ⊆ upperHalfPlane)
    (f : ℂ → ℝ≥0∞) (hf : Measurable f) (A : Set Ω)
…

    Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.upperHalfPlane