NormalizedRestartKernel.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Centered-density domination for the actual capacity-normalized restart. The fresh marked point has unit modulus in the application; its source radius level is transported to the original physical radius level.

def OAI.SLEExactGauge.normalizedRestartDriver line 16
lemma OAI.SLEExactGauge.normalized_restart_witness line 19
lemma OAI.SLEExactGauge.initialGreen_pos_real_mul line 37

theorem OAI.SLEExactGauge.IsCapacityTwoWitness.normalized_restart_stopped_green_lower line 48

Source documentation

The normalized fresh finite-centered density is dominated by the terminal physical density, relative to the density at the actual past stop.

theorem IsCapacityTwoWitness.normalized_restart_stopped_green_lower
    {U : ℝ≥0 → ℝ} {γ β : ℝ≥0 → ℂ} {G F G' F' : ℝ≥0 → ℂ → ℂ}
    (hw : IsCapacityTwoWitness U γ G F) (hU : Continuous U) (T a : ℝ≥0) (ha : 0 < a)
    (hb : IsCapacityTwoWitness (normalizedRestartDriver U T a) β G' F')
    (κ : ℝ) (w : ℂ) (hwH : w ∈ upperHalfPlane) (u v : ℝ)
    (hbase : fullRadius G T (F T ((a : ℂ) * w + (U T : ℂ))) =
      (2 * (F T ((a : ℂ) * w + (U T : ℂ))).im) * Real.exp (-u)) :
    greenDensity κ U γ G T (F T ((a : ℂ) * w + (U T : ℂ))) *
        (stoppedGreen κ (normalizedRestartDriver U T a) β G' w v / initialGreen κ w) ≤
      stoppedGreen κ U γ G (F T ((a : ℂ) * w + (U T : ℂ))) (u + v) := by
…

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