OAI/Probability/SLE/Mass/RestartStoppedMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SLEExactGauge.segmentSausageCharge_clock_le line 16
2. lemma OAI.SLEExactGauge.stoppedWholeSausageCharge_clock_le line 27
3. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.normalized_restart_level_of_live_source line 37
4. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.normalized_restart_stopped_mass_le line 65

   Source documentation

   At every finite source radius level, the stopped fresh physical mass is contained in the stopped original mass at the corresponding actual level.

   theorem IsCapacityTwoWitness.normalized_restart_stopped_mass_le
       {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 : ℂ) (u q : ℝ)
       (hbase : fullRadius G T (F T ((a : ℂ) * w + (U T : ℂ))) =
         (2 * (F T ((a : ℂ) * w + (U T : ℂ))).im) * Real.exp (-u))
       (η : C(ℝ≥0, ℂ)) (hpath : ∀ t, η t = γ (T + a ^ 2 * t))
       (hfinite : radiusLevelTime β G' w q < ∞) (κ v : ℝ) (D : Set ℂ) :
       stoppedWholeSausageCharge κ η (radiusLevelTime β G' w q) v D ≤
         stoppedWholeSausageCharge κ ⟨γ, hw.1⟩
           (radiusLevelTime γ G (F T ((a : ℂ) * w + (U T : ℂ))) (u + q)) v D := by
   …

   Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.normalizedRestartDriver, OAI.SLEExactGauge.fullRadius, OAI.SLEExactGauge.radiusLevelTime, OAI.SLEExactGauge.stoppedWholeSausageCharge