CubeEuclideanL8

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

The Euclidean normalized L^p carrier of e.nablaw.in.L.eight

ABK26's display e.nablaw.in.L.eight is written with the Euclidean pointwise length of a vector field, under the manuscript's volume-normalized cube average. The project ambient carrier is Vec d = Fin d -> ℝ, whose NormedAddCommGroup instance is the sup norm, so Homogenization.cubeLpNorm Q p (f : Vec d -> Vec d) reads the display in the sup gauge. This module records the Euclidean reading explicitly and proves the two-sided comparison between the two gauges, so that no reading choice is made silently anywhere downstream.

Main definitions

• cubeEuclideanLpNorm Q p f -- the manuscript's ‖f‖_{L^p(Q)} under the volume-normalized cube average, defined as the scalar cubeLpNorm of the pointwise Euclidean length Book.Ch02.vecNorm of f.

Main results

• norm_le_vecNorm, vecNorm_le_sqrt_dim_mul_norm -- the pointwise gauge comparison ‖v‖_sup ≤ |v|_2 ≤ sqrt d * ‖v‖_sup.
• cubeLpNorm_le_cubeEuclideanLpNorm, cubeEuclideanLpNorm_le_sqrt_dim_mul_cubeLpNorm -- its L^p form. The two gauges therefore differ by at most sqrt d, which the display's dimension-only constant C(d) absorbs.
• cubeLpNorm_streamIncrementSize_eq_streamIncrementLpNorm -- the identification of the Provider.Stream carrier streamIncrementLpNorm p l n m, which is built from the Euclidean matrix operator norm and Book.Ch02.average, with a scalar cubeLpNorm on the origin cube.
• memLp_normalizedCubeMeasure_of_continuous -- every continuous field lies in every L^p of a normalized cube measure.

References

• ABK26, e.nablaw.in.L.eight.
• ABK26, e.km.kn.Lp.

The pointwise gauge comparison

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.norm_le_vecNorm {d : ℕ} (v : HCPolySupport.Vec d) : ‖v‖ ≤ HCPolySupport.Book.Ch02.vecNorm v

The ambient sup norm of Vec d is below the Euclidean length.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.vecNorm_le_sqrt_dim_mul_norm {d : ℕ} (v : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.vecNorm v ≤ √↑d * ‖v‖

The Euclidean length of Vec d is below sqrt d times the ambient sup norm.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.vecNorm_eq_sqrt_vecNormSq {d : ℕ} (v : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.vecNorm v = √(HCPolySupport.vecNormSq v)

The Euclidean length as a square root of the coordinate sum.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.continuous_vecNorm {d : ℕ} : Continuous HCPolySupport.Book.Ch02.vecNorm

The Euclidean length is continuous.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.memLp_vecNorm_of_memLp {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {p : ENNReal} {u : Omega → HCPolySupport.Vec d} (hu : MeasureTheory.MemLp u p mu) : MeasureTheory.MemLp (fun (x : Omega) => HCPolySupport.Book.Ch02.vecNorm (u x)) p mu

The Euclidean gauge of an Lᵖ vector field is Lᵖ for any measure and exponent.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.integrableOn_cubeSet_of_integrable_normalized {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : HCPolySupport.TriadicCube d) {g : HCPolySupport.Vec d → E} (hg : MeasureTheory.Integrable g (HCPolySupport.normalizedCubeMeasure Q)) : MeasureTheory.IntegrableOn g (HCPolySupport.cubeSet Q) MeasureTheory.volume

Integrability for normalized cube measure gives Lebesgue integrability on the half-open cube.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.integrableOn_cubeSet_vecNormSq_sq_of_memLp_four {d : ℕ} (Q : HCPolySupport.TriadicCube d) {u : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : MeasureTheory.MemLp u 4 (HCPolySupport.normalizedCubeMeasure Q)) : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (u x) ^ 2) (HCPolySupport.cubeSet Q) MeasureTheory.volume

An L⁴ field has integrable squared energy on the half-open cube.

Elementary cubeLpNorm A

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.cubeLpNorm_mono_of_memLp {d : ℕ} {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] (Q : HCPolySupport.TriadicCube d) (p : ENNReal) {f : HCPolySupport.Vec d → E} {g : HCPolySupport.Vec d → F} (hfg : ∀ (x : HCPolySupport.Vec d), ‖f x‖ ≤ ‖g x‖) (hg : MeasureTheory.MemLp g p (HCPolySupport.normalizedCubeMeasure Q)) : HCPolySupport.cubeLpNorm Q p f ≤ HCPolySupport.cubeLpNorm Q p g

Pointwise domination transfers to cubeLpNorm, provided the dominating field has finite norm.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.cubeLpNorm_const_mul_of_nonneg {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : HCPolySupport.TriadicCube d) (p : ENNReal) {c : ℝ} (hc : 0 ≤ c) (f : HCPolySupport.Vec d → E) : (HCPolySupport.cubeLpNorm Q p fun (x : HCPolySupport.Vec d) => c • f x) = c * HCPolySupport.cubeLpNorm Q p f

cubeLpNorm of a nonnegative constant multiple of a field.

The Euclidean normalized cube norm

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.cubeEuclideanLpNorm {d : ℕ} (Q : HCPolySupport.TriadicCube d) (p : ENNReal) (f : HCPolySupport.Vec d → HCPolySupport.Vec d) : ℝ

The manuscript's volume-normalized L^p norm of a vector field, read with the Euclidean pointwise length, as in e.nablaw.in.L.eight.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.Corrector.cubeEuclideanLpNorm Q p f = HCPolySupport.cubeLpNorm Q p fun (x : HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.vecNorm (f x)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.cubeEuclideanLpNorm_nonneg {d : ℕ} (Q : HCPolySupport.TriadicCube d) (p : ENNReal) (f : HCPolySupport.Vec d → HCPolySupport.Vec d) : 0 ≤ cubeEuclideanLpNorm Q p f

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.cubeLpNorm_le_cubeEuclideanLpNorm {d : ℕ} (Q : HCPolySupport.TriadicCube d) (p : ENNReal) (f : HCPolySupport.Vec d → HCPolySupport.Vec d) (hf : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.vecNorm (f x)) p (HCPolySupport.normalizedCubeMeasure Q)) : HCPolySupport.cubeLpNorm Q p f ≤ cubeEuclideanLpNorm Q p f

The sup-gauge cube norm is below the Euclidean one.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.cubeEuclideanLpNorm_le_sqrt_dim_mul_cubeLpNorm {d : ℕ} (Q : HCPolySupport.TriadicCube d) (p : ENNReal) (f : HCPolySupport.Vec d → HCPolySupport.Vec d) (hf : MeasureTheory.MemLp f p (HCPolySupport.normalizedCubeMeasure Q)) : cubeEuclideanLpNorm Q p f ≤ √↑d * HCPolySupport.cubeLpNorm Q p f

The Euclidean cube norm is below sqrt d times the sup-gauge one.

MemLp for continuous fields on a normalized cube

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.memLp_normalizedCubeMeasure_of_continuous {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : HCPolySupport.TriadicCube d) (p : ENNReal) {f : HCPolySupport.Vec d → E} (hf : Continuous f) : MeasureTheory.MemLp f p (HCPolySupport.normalizedCubeMeasure Q)

Every continuous field lies in every L^p of a normalized cube measure: the measure is finite and supported in a bounded set.

The stream-increment carrier as a cubeLpNorm

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.streamIncrementSize {d : ℕ} (n m : ℤ) (omega : Cutoff.ShellSeq d) (x : HCPolySupport.Vec d) : ℝ

The scalar field whose cubeLpNorm is the manuscript's ‖k_m - k_n‖_{L^p(cu_l)}: the pointwise Euclidean operator norm of the stream increment.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.streamIncrementSize_nonneg {d : ℕ} (n m : ℤ) (omega : Cutoff.ShellSeq d) (x : HCPolySupport.Vec d) : 0 ≤ streamIncrementSize n m omega x

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.continuous_streamIncrementSize {d : ℕ} (n m : ℤ) (omega : Cutoff.ShellSeq d) : Continuous (streamIncrementSize n m omega)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.cubeLpNorm_streamIncrementSize_eq_streamIncrementLpNorm {d : ℕ} {p : ℝ} (hp : 0 < p) (l n m : ℤ) (omega : Cutoff.ShellSeq d) : HCPolySupport.cubeLpNorm (HCPolySupport.originCube d l) (ENNReal.ofReal p) (streamIncrementSize n m omega) = Stream.streamIncrementLpNorm p l n m omega

The identification of the two L^p carriers. The Provider.Stream norm streamIncrementLpNorm p l n m, built from Book.Ch02.average over the open origin cube and the Euclidean matrix operator norm, is the cubeLpNorm of the scalar field streamIncrementSize on the same cube.