WeightedTransportEnergy.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Absorbing both errors in the weak transport balance

theorem OAI.RegularPointCoordinates.weighted_transport_energy line 17

Source documentation

Integration and two weighted Young inequalities give a quadratic bound. All weights and the weak balance are explicit; the radial cutoff supplies them in the application. In particular no division by the inner norm occurs.

theorem weighted_transport_energy (B : Set X) (hB : MeasurableSet B)
    {w e F χ ρ ζ K : X → ℝ} {C Dχ Dρ Dζ A : ℝ}
    (hw : MemLp w 2 μ) (he : MemLp e 2 μ) (hF : MemLp F 2 μ)
    (hχ : AEStronglyMeasurable χ μ) (hρ : AEStronglyMeasurable ρ μ)
    (hζ : AEStronglyMeasurable ζ μ)
    (hwbound : ∀ᵐ x ∂μ, |w x| ≤ C)
    (hχbound : ∀ᵐ x ∂μ, 0 ≤ χ x ∧ χ x ≤ Dχ)
    (hρbound : ∀ᵐ x ∂μ, 0 ≤ ρ x ∧ ρ x ≤ Dρ)
    (hζbound : ∀ᵐ x ∂μ, 0 ≤ ζ x ∧ ζ x ≤ Dζ)
    (hK : Integrable (fun x => K x * (w x) ^ 2) μ)
    (hcoerce : ∀ᵐ x ∂μ, ζ x ≤ A * B.indicator (fun _ => (1 : ℝ)) x - K x + ρ x * e x)
    (hχcompare : ∀ᵐ x ∂μ, χ x ≤ ζ x + Dχ * B.indicator (fun _ => (1 : ℝ)) x)
…