Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section24.UnitCubeSkewW2Infinity.ValueL2

ValueL2 #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Characterization of the frozen L² value norm #

Algsuperdiff.Frozen.Section24.UnitCubeSkewW2Infinity.valueL2 is defined as an eLpNorm of the pointwise Euclidean matrix norm of the frozen field over the unit cube. This module is the ordinary A sitting immediately beside that frozen definition, in the same style as Algsuperdiff.Section24.UnitCubeMultiscale.*.Characterization: it names the pointwise norm field (matrixNormField), supplies its measurability and L² membership on the carrier, and unfolds the frozen definition exactly once, in valueL2_sq_eq_integral.

Every downstream consumer routes through valueL2_sq_eq_integral; no provider module ever delta-unfolds valueL2 again.

This module imports only Mathlib, Homogenization, and frozen definition files. In particular it imports no Section 2.4 provider module: that layering is the point of keeping the characterization here.

The unit cube carries a finite measure #

Measurability of the Euclidean matrix norm #

source
theorem Algsuperdiff.Section24.UnitCubeSkewW2Infinity.lipschitzWith_matrixNorm {d : ℕ} :
LipschitzWith (↑d ^ 2) fun (A : HCPolySupport.Mat d) => HCPolySupport.Book.Ch02.matrixNorm A

The Chapter 2 matrix norm is Lipschitz for the entrywise supremum norm.

source
theorem Algsuperdiff.Section24.UnitCubeSkewW2Infinity.continuous_matrixNorm {d : ℕ} :
Continuous fun (A : HCPolySupport.Mat d) => HCPolySupport.Book.Ch02.matrixNorm A
source
theorem Algsuperdiff.Section24.UnitCubeSkewW2Infinity.aestronglyMeasurable_of_entries {d : ℕ} {μ : MeasureTheory.Measure (HCPolySupport.Vec d)} {F : HCPolySupport.Vec d → HCPolySupport.Mat d} (hent : ∀ (i j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : HCPolySupport.Vec d) => F x i j) μ) :
MeasureTheory.AEStronglyMeasurable F μ

A matrix-valued function with a.e. strongly measurable entries is a.e. strongly measurable.

The pointwise Euclidean matrix norm of the frozen field #

source
noncomputable def Algsuperdiff.Section24.UnitCubeSkewW2Infinity.matrixNormField {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) :
HCPolySupport.Vec d → ℝ

The pointwise Euclidean matrix norm of the frozen field.

Equations
Instances For
    source
    theorem Algsuperdiff.Section24.UnitCubeSkewW2Infinity.matrixNormField_nonneg {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (x : HCPolySupport.Vec d) :
    0 ≤ matrixNormField h x
    source
    theorem Algsuperdiff.Section24.UnitCubeSkewW2Infinity.aestronglyMeasurable_matrixNormField_carrier {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) :
    MeasureTheory.AEStronglyMeasurable (matrixNormField h) (HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier)
    source
    theorem Algsuperdiff.Section24.UnitCubeSkewW2Infinity.memLp_matrixNormField_two_carrier {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) :
    MeasureTheory.MemLp (matrixNormField h) 2 (HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier)

    The pointwise norm field is square integrable on the unit cube: it is dominated by the sum of the absolute values of the frozen entries, and each entry is in L^∞ hence — the carrier being finite — in L².

    The characterization of the frozen L² value norm #

    source
    theorem Algsuperdiff.Section24.UnitCubeSkewW2Infinity.valueL2_sq_eq_integral {d : ℕ} (h : Frozen.Section24.UnitCubeSkewW2Infinity d) :
    h.valueL2 ^ 2 = ∫ (x : HCPolySupport.Vec d), matrixNormField h x ^ 2 ∂HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier

    The frozen L² value norm is the mean square of |h| on the unit cube. This is the only place where UnitCubeSkewW2Infinity.valueL2 is unfolded.