Documentation

LeanPool.CaffarelliKohnNirenberg.Foundation.Harmonic.Commutator.SphereTransport

Sphere Transport #

Supporting estimates for the Navier–Stokes development.

source
@[reducible, inline]
abbrev CKN.Foundation.Harmonic.Commutator.E :
Type

The Euclidean three-vector space equipped with the transported L² norm.

Equations
Instances For
    source
    theorem CKN.Foundation.Harmonic.Commutator.vecEuclideanNorm_eq_l2 (z : Vec 3) :
    vecEuclideanNorm z = ‖WithLp.toLp 2 z‖

    The native Euclidean length agrees with the transported `L²` norm.

    source
    theorem CKN.Foundation.Harmonic.Commutator.integral_vecEuclideanNorm_radial (f : ℝ → ℝ) :
    ∫ (z : Vec 3), f (vecEuclideanNorm z) = 4 * Real.pi * ∫ (y : ℝ) in Set.Ioi 0, y ^ 2 * f y

    Radial integration on the native three-dimensional carrier.

    source
    theorem CKN.Foundation.Harmonic.Commutator.integrable_vecEuclideanNorm_radial_iff {f : ℝ → ℝ} :
    MeasureTheory.Integrable (fun (z : Vec 3) => f (vecEuclideanNorm z)) MeasureTheory.volume ↔ MeasureTheory.IntegrableOn (fun (y : ℝ) => y ^ 2 * f y) (Set.Ioi 0) MeasureTheory.volume

    Integrability of a native radial function is equivalent to its polar radial integrability.

    source
    def CKN.Foundation.Harmonic.Commutator.sphereToVec (w : ↑(Metric.sphere 0 1)) :
    Vec 3

    The map that represents points of the transported unit sphere as native three-vectors.

    Equations
    Instances For
      source
      noncomputable def CKN.Foundation.Harmonic.Commutator.vecEuclideanSphereMeasure :
      MeasureTheory.Measure (Vec 3)

      The unit-sphere measure transported back to the native three-dimensional carrier.

      Equations
      Instances For
        source
        theorem CKN.Foundation.Harmonic.Commutator.integral_vec_gaussian_homogeneous (F : Vec 3 → ℝ) (hF : MeasureTheory.AEStronglyMeasurable F vecEuclideanSphereMeasure) (hhom : ∀ (r : ℝ), 0 < r → ∀ (z : Vec 3), F (r • z) = r ^ 4 * F z) :
        ∫ (z : Vec 3), F z * Real.exp (-vecNormSq z) = (∫ (z : Vec 3), F z ∂vecEuclideanSphereMeasure) * ∫ (r : ↑(Set.Ioi 0)), ↑r ^ 4 * Real.exp (-↑r ^ 2) ∂MeasureTheory.Measure.volumeIoiPow 2

        A homogeneous degree-four Gaussian integral factors through the transported sphere.