ConformalMassTransport.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The weighted pushforward used for canonical mass in a conformal image. Compact tests pull back with the same deterministic convex sequence; the construction does not extract a new subsequence for the image domain.

def OAI.SLEExactGauge.Multipoint.conformalMass line 21
Source documentation
For a conformal identification, w is the continuous weight |J'|^d.
```
def conformalMass (J : upperHalfPlane ≃ₜ D) (w : C(upperHalfPlane, ℝ≥0))
    (μ : Measure upperHalfPlane) : Measure D :=
…
```
Mentions: OAI.SLEExactGauge.upperHalfPlane
def OAI.SLEExactGauge.Multipoint.conformalMassTest line 25
lemma OAI.SLEExactGauge.Multipoint.conformalMassTest_apply line 30
lemma OAI.SLEExactGauge.Multipoint.conformalMass_integral line 34
lemma OAI.SLEExactGauge.Multipoint.conformalMass_radon line 42
lemma OAI.SLEExactGauge.Multipoint.conformalMass_measurable line 51
lemma OAI.SLEExactGauge.Multipoint.conformalMass_zero line 61
lemma OAI.SLEExactGauge.Multipoint.conformalMass_add line 65
lemma OAI.SLEExactGauge.Multipoint.conformalMass_mono line 71
lemma OAI.SLEExactGauge.Multipoint.conformalMass_nullSingleton line 80
lemma OAI.SLEExactGauge.Multipoint.conformalMass_carried line 96

lemma OAI.SLEExactGauge.Multipoint.conformalMass_test_tendsto line 107

Source documentation

Vague convergence transfers for every image-domain test on the same event and with the same sequence.

lemma conformalMass_test_tendsto (J : upperHalfPlane ≃ₜ D)
    (w : C(upperHalfPlane, ℝ≥0)) (μ : ℕ → Measure upperHalfPlane)
    (ν : Measure upperHalfPlane)
    (h : ∀ f : C_c(upperHalfPlane, ℝ),
      Tendsto (fun n => ∫ z, f z ∂μ n) atTop (𝓝 (∫ z, f z ∂ν)))
    (f : C_c(D, ℝ)) :
    Tendsto (fun n => ∫ z, f z ∂conformalMass J w (μ n)) atTop
      (𝓝 (∫ z, f z ∂conformalMass J w ν)) := by
…

Mentions: OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.Multipoint.conformalMass

lemma OAI.SLEExactGauge.Multipoint.conformalMass_test_continuous line 118