RibbonStoppedMassTransport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact spatial and capacity transport of a completed ribbon's stopped mass. The completion is the actual first front of the transported trace.

lemma OAI.SLEExactGauge.firstFrontTime_scalePath_of_finite line 20
lemma OAI.SLEExactGauge.segmentSausageCharge_scalePath line 35
def OAI.SLEExactGauge.ribbonStoppedMassEvent line 53
lemma OAI.SLEExactGauge.measurableSet_ribbonStoppedMassEvent line 59

theorem OAI.SLEExactGauge.mem_ribbonStoppedMassEvent_scalePath line 80

Source documentation

Transport uses the same actual completed prefix and a deterministically scaled mesh, region and mass threshold.

theorem mem_ribbonStoppedMassEvent_scalePath
    (c : ℝ≥0) (hc : 0 < c) (p : C(ℝ≥0, ℂ)) (P : ℂ → ℂ)
    (g g' : C(ℂ, ℝ)) (hgg' : ∀ z : ℂ, g' ((c : ℂ) * z) = g z)
    (k ε κ : ℝ) {v : ℝ} (hv : 0 < v) (D : Set ℂ) (b : ℝ≥0∞)
    (hp : p ∈ ribbonStoppedMassEvent P g k ε κ v D b) :
    scalePath c p ∈ ribbonStoppedMassEvent (fun z => (c : ℂ) * P z) g' k ε κ
      ((c : ℝ) * v) (affine 0 c '' D) (ENNReal.ofReal ((c : ℝ) ^ dimension κ) * b) := by
…

Mentions: OAI.SLEExactGauge.ribbonStoppedMassEvent, OAI.SLEExactGauge.dimension