Documentation

LeanPool.Superdiffusion.Support.Sobolev.Fractional.EuclideanWspSmoothDualNegativeBesov

EuclideanWspSmoothDualNegativeBesov #

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Scalar-coordinate envelopes for the source negative Besov seminorm #

This module keeps the source-facing vector negative Besov seminorm distinct from the scalar circ quantities used by the projection duality argument. It only records the elementary coordinate envelope: each scalar coordinate of a vector field has no larger running-scale block-average envelope.

source
noncomputable def HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovScalarDepthEnergy {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) (i : Fin d) (j : ℕ) :
ENNReal

The scalar running-scale depth energy of one coordinate of the represented L² field. This is deliberately an auxiliary envelope, not a redefinition of the source-facing vector seminorm.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovScalarPartialENorm {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) (i : Fin d) (N : ℕ) :
    ENNReal

    Finite-depth scalar circ envelope, with the same running-scale weights as the source negative Besov quantity.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovScalarENorm {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) (i : Fin d) :
      ENNReal

      The infinite scalar circ envelope of a coordinate, retained separately from the vector source seminorm.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovScalarDepthEnergy_le {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) (i : Fin d) (j : ℕ) :
        cubeEuclideanNegativeBesovScalarDepthEnergy Q s p F i j ≤ cubeEuclideanNegativeBesovDepthEnergy Q s p F j
        source
        theorem HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovScalarPartialENorm_le {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) (i : Fin d) (N : ℕ) :
        cubeEuclideanNegativeBesovScalarPartialENorm Q s p F i N ≤ cubeEuclideanNegativeBesovESeminorm Q s p F
        source
        theorem HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovScalarENorm_le {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) (i : Fin d) :
        cubeEuclideanNegativeBesovScalarENorm Q s p F i ≤ cubeEuclideanNegativeBesovESeminorm Q s p F