IncrementBridge

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

From the increment oscillation gauge to the Section 2.4 sensitivity gate

The frozen Section 2.4 sensitivity lemmas gate on UnitCubeSkewW2Infinity.gradientW1Infinity, the volume-normalized W^{1,infinity} gradient norm on the literal unit cube. ABK26's consumer p.bfA.multiscalebound feeds the stream increment h := k_L - k_j, rescaled from z + square_j to the unit cube, into that gate.

This module builds the rescaled object and computes the exact normalization. For a shell field h the rescaled unit-cube field is y |-> h(z + 3^j y), whose derivatives carry the chain-rule factors 3^j and 3^{2j}; consequently

gradientW1Infinity <= max { 3^{2j} ||grad² h||_{L∞(z+square_j)}, 3^{j} ||grad h||_{L∞(z+square_j)} } = 3^{2j} ||grad h||_{W^{1,infinity}(z+square_j)},

which is exactly incrementOscGauge. The factors are exact: the |U|^{-1/d} of ABK26 at a cube of side 3^j is 3^{-j}.

Main definitions

• shellFieldUnitCube: the unit-cube W^{2,infinity} package of a shell field, carrying the shell's own stored derivatives.

Main results

• frozen_matrixDerivativeNorm_eq, frozen_matrixSecondDerivativeNorm_eq: the frozen Section 2.4 matrix-derivative norms are the shell-field ones.
• gradientW1Infinity_shellFieldUnitCube_le: the gate quantity is below the raw unit-cube derivative gauges of the shell field.

References

• ABK26 (volume-normalized Sobolev norms).
• ABK26, e.Bosc.def.
• ABK26, e.we.can.apply.cg.

theorem Algsuperdiff.Section3.Provider.BadEvents.instIsNormableSpaceRealMat (d : ℕ) : IsNormableSpace ℝ (HCPolySupport.Mat d)

theorem Algsuperdiff.Section3.Provider.BadEvents.instIsNormableSpaceRealContinuousLinearMapIdVecMat (d : ℕ) : IsNormableSpace ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Entry and evaluation continuous linear maps

def Algsuperdiff.Section3.Provider.BadEvents.entryLinearMap {d : ℕ} (i j : Fin d) : HCPolySupport.Mat d →ₗ[ℝ] ℝ

Extract a matrix entry as a linear functional.

Equations

• Algsuperdiff.Section3.Provider.BadEvents.entryLinearMap i j = { toFun := fun (A : HCPolySupport.Mat d) => A i j, map_add' := ⋯, map_smul' := ⋯ }

def Algsuperdiff.Section3.Provider.BadEvents.entryCLM {d : ℕ} (i j : Fin d) : HCPolySupport.Mat d →L[ℝ] ℝ

Extract a matrix entry as a continuous linear functional.

Equations

• Algsuperdiff.Section3.Provider.BadEvents.entryCLM i j = { toLinearMap := Algsuperdiff.Section3.Provider.BadEvents.entryLinearMap i j, cont := ⋯ }

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.evalCLM {d : ℕ} (v : HCPolySupport.Vec d) : (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) →L[ℝ] HCPolySupport.Mat d

Evaluate a first derivative at a fixed direction as a continuous linear map.

Equations

• Algsuperdiff.Section3.Provider.BadEvents.evalCLM v = (ContinuousLinearMap.apply ℝ (HCPolySupport.Mat d)) v

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.evalCLM₂ {d : ℕ} (v : HCPolySupport.Vec d) : (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d

Evaluate a second derivative at its first direction as a continuous linear map.

Equations

• Algsuperdiff.Section3.Provider.BadEvents.evalCLM₂ v = (ContinuousLinearMap.apply ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)) v

Essential boundedness on the literal unit cube

theorem Algsuperdiff.Section3.Provider.BadEvents.memLp_top_on_unitCube {d : ℕ} {f : HCPolySupport.Vec d → ℝ} (hf : Continuous f) : MeasureTheory.MemLp f ⊤ (HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier)

Regularity of the entries of a shell field

theorem Algsuperdiff.Section3.Provider.BadEvents.continuous_entry {d : ℕ} (g : Frozen.Assumptions.ShellField d) (i j : Fin d) : Continuous fun (x : HCPolySupport.Vec d) => (↑g).1 x i j

theorem Algsuperdiff.Section3.Provider.BadEvents.continuous_deriv_entry {d : ℕ} (g : Frozen.Assumptions.ShellField d) (k i j : Fin d) : Continuous fun (x : HCPolySupport.Vec d) => (g.deriv x) (HCPolySupport.basisVec k) i j

theorem Algsuperdiff.Section3.Provider.BadEvents.continuous_secondDeriv_entry {d : ℕ} (g : Frozen.Assumptions.ShellField d) (l k i j : Fin d) : Continuous fun (x : HCPolySupport.Vec d) => ((g.secondDeriv x) (HCPolySupport.basisVec l)) (HCPolySupport.basisVec k) i j

theorem Algsuperdiff.Section3.Provider.BadEvents.hasFDerivAt_entry {d : ℕ} (g : Frozen.Assumptions.ShellField d) (i j : Fin d) (x : HCPolySupport.Vec d) : HasFDerivAt (fun (y : HCPolySupport.Vec d) => (↑g).1 y i j) (entryCLM i j ∘SL g.deriv x) x

theorem Algsuperdiff.Section3.Provider.BadEvents.hasFDerivAt_deriv_entry {d : ℕ} (g : Frozen.Assumptions.ShellField d) (k i j : Fin d) (x : HCPolySupport.Vec d) : HasFDerivAt (fun (y : HCPolySupport.Vec d) => (g.deriv y) (HCPolySupport.basisVec k) i j) ((entryCLM i j ∘SL evalCLM (HCPolySupport.basisVec k)) ∘SL g.secondDeriv x) x

theorem Algsuperdiff.Section3.Provider.BadEvents.contDiff_one_entry {d : ℕ} (g : Frozen.Assumptions.ShellField d) (i j : Fin d) : ContDiff ℝ 1 fun (x : HCPolySupport.Vec d) => (↑g).1 x i j

theorem Algsuperdiff.Section3.Provider.BadEvents.contDiff_one_deriv_entry {d : ℕ} (g : Frozen.Assumptions.ShellField d) (k i j : Fin d) : ContDiff ℝ 1 fun (x : HCPolySupport.Vec d) => (g.deriv x) (HCPolySupport.basisVec k) i j

The unit-cube W^{2,infinity} package of a shell field

def Algsuperdiff.Section3.Provider.BadEvents.shellFieldUnitCube {d : ℕ} (g : Frozen.Assumptions.ShellField d) : Frozen.Section24.UnitCubeSkewW2Infinity d

The unit-cube W^{2,infinity} skew package of a shell field, carrying the shell's own stored first and second derivatives.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algsuperdiff.Section3.Provider.BadEvents.shellFieldUnitCube_firstDeriv {d : ℕ} (g : Frozen.Assumptions.ShellField d) (x : HCPolySupport.Vec d) : (shellFieldUnitCube g).firstDeriv x = g.deriv x

@[simp]

theorem Algsuperdiff.Section3.Provider.BadEvents.shellFieldUnitCube_secondDeriv {d : ℕ} (g : Frozen.Assumptions.ShellField d) (x : HCPolySupport.Vec d) : (shellFieldUnitCube g).secondDeriv x = g.secondDeriv x

@[simp]

theorem Algsuperdiff.Section3.Provider.BadEvents.shellFieldUnitCube_value {d : ℕ} (g : Frozen.Assumptions.ShellField d) (x : HCPolySupport.Vec d) : ↑↑(shellFieldUnitCube g).toLInfSkewMatrixFieldOn x = (↑g).1 x

The frozen Section 2.4 matrix-derivative norms are the shell-field ones

theorem Algsuperdiff.Section3.Provider.BadEvents.frozen_matrixDerivativeNorm_eq {d : ℕ} (D : Frozen.Assumptions.ShellField.MatrixDerivative d) : Frozen.Section24.matrixDerivativeNorm D = Frozen.Assumptions.ShellField.matrixDerivativeNorm D

theorem Algsuperdiff.Section3.Provider.BadEvents.frozen_matrixSecondDerivativeNorm_eq {d : ℕ} (H : Frozen.Assumptions.ShellField.MatrixSecondDerivative d) : Frozen.Section24.matrixSecondDerivativeNorm H = Frozen.Assumptions.ShellField.matrixSecondDerivativeNorm H

The gate quantity of a shell field's unit-cube package

theorem Algsuperdiff.Section3.Provider.BadEvents.toReal_eLpNorm_unitCube_le {d : ℕ} {f : HCPolySupport.Vec d → ℝ} {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d 0), ‖f x‖ ≤ C) : (MeasureTheory.eLpNorm f ⊤ (HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)).carrier)).toReal ≤ C

A pointwise unit-cube bound controls the real-valued essential-supremum norm.

theorem Algsuperdiff.Section3.Provider.BadEvents.gradientW1Infinity_shellFieldUnitCube_le {d : ℕ} (g : Frozen.Assumptions.ShellField d) : (shellFieldUnitCube g).gradientW1Infinity ≤ max g.unitCubeSecondDerivNorm g.unitCubeDerivNorm

The Section 2.4 gate quantity of a shell field's unit-cube package is below the raw unit-cube derivative gauges of the shell field.