MeasuredDensitySources.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual bounded-density source measures for Euclidean transport tests

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.measured_density_sources_nonzero line 15

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.measured_density_sources line 74

Source documentation

Original interface retained for existing callers.

theorem NoncollapsedRCD.measured_density_sources {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) {S : ℝ} (hS : 0<S)
    (p : ℕ → X) (r ε : ℕ → ℝ) (v : ℕ → X → Euclidean n)
    (hr : ∀ k, 0<r k) (hε : Tendsto ε atTop (𝓝 0))
    (hv : ∀ k, IsMeasuredEuclideanApproximation (hausdorff n X) n (p k) (r k) S (ε k) (v k))
    (a : Euclidean n →ᵇ ℝ) (ha : ∀ z, 0≤a z)
    (hpos : 0<∫ z, a z ∂(euclideanBallProbability n S : Measure (Euclidean n))) :
    ∃ N : ℕ, ∃ ν : ℕ → ProbabilityMeasure X, ∃ c : ℕ → ℝ,
      (∀ k, 0≤c k) ∧
      Tendsto c atTop (𝓝 ((∫ z, a z ∂(euclideanBallProbability n S : Measure (Euclidean n)))⁻¹*‖a‖)) ∧
      (∀ k, (ν k : Measure X)≤
        (ENNReal.ofReal (c k)*(hausdorff n X (ball (p (k+N)) (S*r (k+N))))⁻¹) • hausdorff n X) ∧
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsMeasuredEuclideanApproximation, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.euclideanBallProbability