RadialTransportIdentity.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The weak transport identity tested on the unnormalized residual

theorem OAI.RegularPointCoordinates.radial_transport_weak_identity line 20

Source documentation

The actual compact test χ w² is admissible in the local constant Laplacian equation. This proves the transport balance before any division by the inner-ball norm of w.

theorem radial_transport_weak_identity (Ω : Set X) (hΩ : MeasurableSet Ω)
    (f w η : SobolevSpace μ hQ) {a : ℝ}
    (hf : IsConstantLaplacianOn μ hQ Ω f a) (C D L : ℝ≥0)
    (hw : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ w x| ≤ C)
    (χ : X → ℝ) (hχ : LipschitzWith L χ) (hcpt : HasCompactSupport χ)
    (hbound : ∀ x, |χ x| ≤ D) (hnonneg : ∀ x, 0 ≤ χ x)
    (hsupp : tsupport χ ⊆ Ω) (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ] χ) :
    (∫ x in Ω, 2 * χ x * SobolevSpace.toLp μ hQ w x * localGamma μ hQ f w x +
      (SobolevSpace.toLp μ hQ w x) ^ 2 * localGamma μ hQ f η x ∂μ) =
      -a * ∫ x in Ω, χ x * (SobolevSpace.toLp μ hQ w x) ^ 2 ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma