PrincipalResponseDisplayTwoGrid

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

Binder descriptions below are an informal inventory only, NOT a source certification; certification vocabulary is reserved for frozen source-facing declarations.

Provider: the grid re-assembly behind display 2 of leg (iv)

Display 2 of leg (iv) of l.approximate.recurrence.formula is

  ( avsum_{z in 3^n Zd cap cu_K} E[ | bfAhom_{m-1}^{1/2} P_z |^4 ] )^{1/4} <= C .

Sub-step (ii) (ellipticityBudget_eq, module PrincipalResponseLegsBudgetEllipticity) collapses the integrand into the raw averaged slope pair, so what has to be estimated on the grid is

  avsum_R  | c + (u)_R |^4 ,

with R running over the triadic descendants of cu_K at the localization depth, c one of the two unit directions e, e', and u one of the two fields grad w_D and grad w_N + shom^{-1} h e'. This module reduces that grid average to the single global volume-normalized L^8 norm of u on cu_K, which is the quantity e.nablaw.in.L.eight controls:

  avsum_R | c + (u)_R |^4  <=  8 |c|^4 + 8 ( ‖u‖_{L^8(cu_K)} )^4 .

The three inputs

• the vector Jensen inequality at the fourth power on each subcube, sq_vecNormSq_cubeAverageVec_le_cubeAverage_sq_of_memLp (portable module CubeJensenVec), which replaces |(u)_R|^4 by avg_R |u|^4;
• the grid re-assembly cubeAverage_eq_descendantsAverage_cubeAverage_of_integrableOn of CoarseGraining, which turns the average over subcubes of the subcube averages back into the single average over cu_K;
• the L^4 <= L^8 bridge cubeAverage_vecNormSq_sq_le_cubeLpNorm_eight_vecNorm_pow_four_of_memLp (portable module CubeJensenVec), which is where the volume-normalized L^8 norm of the display appears.

Only one hypothesis is carried: that u lies in L^8 of the normalized cube measure of cu_K. Everything the subcubes need is deduced from it by memLp_normalizedCubeMeasure_of_mem_descendantsAtDepth, which is the statement that a descendant carries at most |cu_K| / |R| times the parent's normalized mass.

The Minkowski step

The second of the two fields is a sum, grad w_N + shom^{-1} h e', whose two summands are controlled separately (the gradient by the Calderon-Zygmund step, the forcing by e.km.kn.Lp). cubeEuclideanLpNorm_add_le is the triangle inequality for the manuscript's Euclidean volume-normalized L^p norm, proved here from the pointwise Euclidean triangle inequality vecNorm_add_le.

Main results

• vecNorm_add_le, cubeEuclideanLpNorm_add_le
• memLp_normalizedCubeMeasure_of_mem_descendantsAtDepth
• descendantsAverage_sq_vecNormSq_add_cubeAverageVec_le

The Euclidean triangle inequality on Vec d

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.vecNorm_add_le {d : ℕ} (a b : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.vecNorm (a + b) ≤ HCPolySupport.Book.Ch02.vecNorm a + HCPolySupport.Book.Ch02.vecNorm b

The Euclidean length on Vec d obeys the triangle inequality.

Minkowski for the Euclidean volume-normalized norm

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeEuclideanLpNorm_add_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) {p : ENNReal} (hp : 1 ≤ p) (f g : HCPolySupport.Vec d → HCPolySupport.Vec d) (hf : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.vecNorm (f x)) p (HCPolySupport.normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.vecNorm (g x)) p (HCPolySupport.normalizedCubeMeasure Q)) : (Corrector.cubeEuclideanLpNorm Q p fun (x : HCPolySupport.Vec d) => f x + g x) ≤ Corrector.cubeEuclideanLpNorm Q p f + Corrector.cubeEuclideanLpNorm Q p g

The triangle inequality for cubeEuclideanLpNorm. The manuscript's Euclidean reading of the volume-normalized L^p norm is a norm: for p >= 1 and two fields whose Euclidean lengths lie in L^p of the normalized cube measure, the norm of the sum is at most the sum of the norms.

Restriction of MemLp to a descendant cube

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.memLp_normalizedCubeMeasure_of_mem_descendantsAtDepth {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {Q R : HCPolySupport.TriadicCube d} {j : ℕ} {p : ENNReal} {f : HCPolySupport.Vec d → E} (hR : R ∈ HCPolySupport.descendantsAtDepth Q j) (hf : MeasureTheory.MemLp f p (HCPolySupport.normalizedCubeMeasure Q)) : MeasureTheory.MemLp f p (HCPolySupport.normalizedCubeMeasure R)

A descendant inherits the parent's L^p membership. The normalized measure of a subcube is dominated by |Q| / |R| times that of the parent, so L^p of the parent's normalized measure sits inside L^p of every descendant's.

MemLp of the Euclidean length

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.memLp_vecNorm_of_memLp {d : ℕ} (Q : HCPolySupport.TriadicCube d) {p : ENNReal} {u : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : MeasureTheory.MemLp u p (HCPolySupport.normalizedCubeMeasure Q)) : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.vecNorm (u x)) p (HCPolySupport.normalizedCubeMeasure Q)

The Euclidean length of an L^p field is L^p: it never exceeds sqrt d times the ambient sup norm.

The grid re-assembly

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.descendantsAverage_sq_vecNormSq_add_cubeAverageVec_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℕ) (c : HCPolySupport.Vec d) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (hu : MeasureTheory.MemLp u 8 (HCPolySupport.normalizedCubeMeasure Q)) : (HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => HCPolySupport.vecNormSq (c + HCPolySupport.cubeAverageVec R u) ^ 2) ≤ 8 * HCPolySupport.vecNormSq c ^ 2 + 8 * Corrector.cubeEuclideanLpNorm Q 8 u ^ 4

The grid form of the fourth power of a shifted cube average.

For a field u in L^8 of the normalized measure of Q, the average over the triadic descendants of Q at any depth j of the fourth power of |c + (u)_R| is bounded by the constant term and the global volume-normalized L^8 norm of u on Q:

  avsum_R | c + (u)_R |^4  <=  8 |c|^4 + 8 ( ‖u‖_{L^8(Q)} )^4 .

The three steps are the vector Jensen inequality on each subcube, the CoarseGraining grid re-assembly of subcube averages, and the volume-normalized L^4 <= L^8 comparison.