RadialTransportEulerIdentity.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The weak transport balance after substituting the Euler equation

theorem OAI.RegularPointCoordinates.radial_transport_euler_identity line 18

Source documentation

Substitution into the proved weak product identity gives the exact balance used by radial transport. The forcing is an actual L2 function.

theorem radial_transport_euler_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 η =ᵐ[μ] χ)
    (F : X → ℝ) (hF : MemLp F 2 μ)
    (heuler : localGamma μ hQ f w =ᵐ[μ.restrict Ω]
      fun x => SobolevSpace.toLp μ hQ w x + F x / 2) :
    (∫ x in Ω, ((a + 2) * χ x + localGamma μ hQ f η x) *
      (SobolevSpace.toLp μ hQ w x) ^ 2 ∂μ) =
…

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