OAI/Probability/SLE/Geometry/RestartGreenKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite centered density after a genuine restart. Only forward composition is needed: a live source radius level gives the physical level, and a source path that never reaches the level contributes zero density.

  1. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.restart_initial_radius line 16
  2. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.restart_inverse_derivative_norm_pos line 28
  3. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.restart_green_composition line 40
  4. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.restart_green_initial line 56
  5. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.restart_level_of_live_source line 68
  6. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.restart_stopped_green_lower line 91

    Source documentation

    Pointwise domination suffices for conditional lower bounds. On every source path which reaches its radius level, this is an equality.

    theorem IsCapacityTwoWitness.restart_stopped_green_lower
    {U : ℝ≥0 → ℝ} {γ β : ℝ≥0 → ℂ} {G F G' F' : ℝ≥0 → ℂ → ℂ}
    (hw : IsCapacityTwoWitness U γ G F) (hU : Continuous U) (T : ℝ≥0)
    (hb : IsCapacityTwoWitness (fun t => U (T + t) - U T) β G' F')
    (κ : ℝ) (z : ℂ) (hz : z ∈ upperHalfPlane) (u v : ℝ)
    (hbase : fullRadius G T (F T (z + (U T : ℂ))) =
      (2 * (F T (z + (U T : ℂ))).im) * Real.exp (-u)) :
    greenDensity κ U γ G T (F T (z + (U T : ℂ))) *
        (stoppedGreen κ (fun t => U (T + t) - U T) β G' z v / initialGreen κ z) ≤
      stoppedGreen κ U γ G (F T (z + (U T : ℂ))) (u + v) := by
…

    Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.fullRadius, OAI.SLEExactGauge.greenDensity, OAI.SLEExactGauge.stoppedGreen, OAI.SLEExactGauge.initialGreen