LocalizationCorrectorRegularity

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

Spatial regularity of the two correctors of e.def.w

The coarse-energy envelope of LocalizationEnvelopeWire.exists_freshShell_gridFourthMoment_mesoWindowEnergy_le_wired asks its caller for four per-sample spatial propositions about the corrector gradient on cu_K:

• MemLp (fun x => vecNorm (grad w x)) 8 (normalizedCubeMeasure cu_K);
• IntegrableOn (fun x => (grad w x k)^2) (openCubeSet cu_K) volume for each coordinate k;
• IntegrableOn (fun x => vecNormSq (grad w x)) (openCubeSet cu_K) volume;
• IntegrableOn (fun x => vecNormSq (grad w x)^2) (openCubeSet cu_K) volume.

None of them is a step of the manuscript's argument: all four are consequences of the single L^8 membership that the Calderon--Zygmund estimate produces alongside its bound, so the caller who already has the weak formulation of e.def.w owes nothing extra. This module derives them.

Main results

• memLp_eight_grad_freshShellDirichlet, memLp_eight_grad_freshShellNeumann -- the L^8 membership of the two corrector gradients at the fresh-shell forcing, read off the external anchor.
• memLp_vecNorm_eight_of_memLp_eight, integrableOn_openCubeSet_vecNormSq_of_memLp_eight, integrableOn_openCubeSet_vecNormSq_sq_of_memLp_eight, integrableOn_openCubeSet_coord_sq_of_memLp_eight -- the four consequences.

The L^8 membership from the external anchor

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.memLp_eight_grad_freshShellDirichlet {d : ℕ} (hd : 2 ≤ d) (Q : HCPolySupport.TriadicCube d) (sigmaInv : ℝ) (omega : Cutoff.ShellSeq d) (n m : ℤ) (e : HCPolySupport.Vec d) (w : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (hw : HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) w fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing sigmaInv omega n m e x) : MeasureTheory.MemLp w.grad 8 (HCPolySupport.normalizedCubeMeasure Q)

The Dirichlet corrector gradient of e.def.w lies in L^8(cu_K). The Calderon--Zygmund estimate produces the membership together with its bound; only the membership is read here.: on hd and on the weak formulation hw of e.def.w.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.memLp_eight_grad_freshShellNeumann {d : ℕ} (hd : 2 ≤ d) (Q : HCPolySupport.TriadicCube d) (sigmaInv : ℝ) (omega : Cutoff.ShellSeq d) (n m : ℤ) (e : HCPolySupport.Vec d) (w : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) (hw : HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) w fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing sigmaInv omega n m e x) : MeasureTheory.MemLp w.toH1Function.grad 8 (HCPolySupport.normalizedCubeMeasure Q)

The Neumann corrector gradient of e.def.w lies in L^8(cu_K). The Neumann mirror of the previous statement.

The four consequences of one L^8 membership

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.memLp_vecNorm_eight_of_memLp_eight {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 gauge of an L^p field is L^p. Unconditional apart from the membership hu.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integrableOn_openCubeSet_vecNormSq_of_memLp_eight {d : ℕ} (Q : HCPolySupport.TriadicCube d) {u : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : MeasureTheory.MemLp u 8 (HCPolySupport.normalizedCubeMeasure Q)) : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (u x)) (HCPolySupport.openCubeSet Q) MeasureTheory.volume

|grad w|^2 is integrable on cu_K.: on hu.

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

|grad w|^4 is integrable on cu_K.: on hu.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integrableOn_openCubeSet_coord_sq_of_memLp_eight {d : ℕ} (Q : HCPolySupport.TriadicCube d) {u : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : MeasureTheory.MemLp u 8 (HCPolySupport.normalizedCubeMeasure Q)) (k : Fin d) : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => u x k ^ 2) (HCPolySupport.openCubeSet Q) MeasureTheory.volume

Each coordinate square of grad w is integrable on cu_K.: on hu.