RadialTransportError.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The quadratic coefficient error in radial transport

The bounded unnormalized residual is used before division by its inner-ball norm. Weighted Young's inequality preserves the square of the Poisson error.

theorem OAI.RegularPointCoordinates.radial_transport_coefficient_error line 20

Source documentation

The transport coefficient error absorbs one quarter of the weighted residual energy and costs the SQUARE of the original Poisson error.

theorem radial_transport_coefficient_error {w e ρ : X → ℝ} {C D : ℝ}
    (hw : MemLp w 2 μ) (he : MemLp e 2 μ) (hρ : AEStronglyMeasurable ρ μ)
    (hwbound : ∀ᵐ x ∂μ, |w x| ≤ C)
    (hρbound : ∀ᵐ x ∂μ, 0 ≤ ρ x ∧ ρ x ≤ D) :
    |∫ x, ρ x * e x * (w x) ^ 2 ∂μ| ≤
      (1 / 4 : ℝ) * (∫ x, ρ x * (w x) ^ 2 ∂μ) +
        C ^ 2 * D * (∫ x, (e x) ^ 2 ∂μ) := by
…

theorem OAI.RegularPointCoordinates.radial_transport_forcing_error line 66

Source documentation

The inhomogeneous forcing term absorbs another quarter of the weighted residual energy. Only its original L2 norm enters the remainder.

theorem radial_transport_forcing_error {w F ρ : X → ℝ} {D : ℝ}
    (hw : MemLp w 2 μ) (hF : MemLp F 2 μ) (hρ : AEStronglyMeasurable ρ μ)
    (hρbound : ∀ᵐ x ∂μ, 0 ≤ ρ x ∧ ρ x ≤ D) :
    |∫ x, ρ x * (w x * F x) ∂μ| ≤
      (1 / 4 : ℝ) * (∫ x, ρ x * (w x) ^ 2 ∂μ) +
        D * (∫ x, (F x) ^ 2 ∂μ) := by
…