ScaledRadialTransportForcing.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Small-radius transport for the actual Sobolev forcing

theorem OAI.RegularPointCoordinates.scaled_radial_derivative_add_representative line 20
Source documentation
Convert the exact local L2 identity into the scalar equation used by the weak divergence test.
```
theorem scaled_radial_derivative_add_representative (Ω : Set X)
    (f w q : SobolevSpace μ hQ) {B : ℝ}
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B)
    (heq : localRadialDerivative μ hQ Ω f hf w = SobolevSpace.restrictLp μ hQ Ω (w + q)) :
    localGamma μ hQ f w =ᵐ[μ.restrict Ω]
      fun x => SobolevSpace.toLp μ hQ w x + SobolevSpace.toLp μ hQ q x := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.localRadialDerivative, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.SobolevSpace.toLp

theorem OAI.RegularPointCoordinates.scaled_radial_transport_sobolev_forcing line 35

Source documentation

The forcing in the projected Euler equation is a Sobolev function. Its square enters the outer bound with a quadratic coefficient, so the residual can later be normalized safely.

theorem scaled_radial_transport_sobolev_forcing {n : ℕ} {R a : ℝ} (hR : 0 < R)
    (ha : 0 ≤ a) (han : a ≤ (n : ℝ) + 1) (z : X)
    (f w q : SobolevSpace μ hQ)
    (hlap : IsConstantLaplacianOn μ hQ (ball z (4 * R)) f a)
    {B : ℝ} (hf : ∀ᵐ x ∂μ.restrict (ball z (4 * R)), localGamma μ hQ f f x ≤ B)
    (C : ℝ≥0) (hw : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ w x| ≤ C)
    (e : X → ℝ) (he : MemLp e 2 μ)
    (heuler : localRadialDerivative μ hQ (ball z (4 * R)) f hf w =
      SobolevSpace.restrictLp μ hQ (ball z (4 * R)) (w + q))
    (hradial : localGamma μ hQ f (inwardSobolev μ hQ z (3 * R))
      =ᵐ[μ.restrict (ball z (3 * R))] fun x => e x - dist z x)
    (hsphere : μ (sphere z R) = 0) :
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localRadialDerivative, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.inwardSobolev