OAI/Geometry/RCD/Transport/RadialTransportEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.radial_transport_annular_energy line 21

   Source documentation

   The annular energy of the original bounded residual has a quadratic bound from its inner norm and the two actual L2 errors. The cutoff and its derivative are constructed, and the balance follows from the weak Laplacian.

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

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