PrincipalResponseIndepAssembly

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

NOTE: this module is an ordinary Provider helper / conditional A. The binder inventories below are informal descriptions only.

The second moment's gauged load

MODULE. It is not imported by Algsuperdiff/Section3.lean and is not part of any build closure.

Sources in ABK26:

• The sentence "Therefore, by independence of bfA_{m-h} and G_{-(h)_{z+cu_n}} P_z (the latter is a function of k_m - k_{m-h}), increasing M in \eqref{e.cgamma.constraints} if necessary,";
• e.nablaw.in.L.eight (label; display);
• e.Pz.def (label; display), the load;
• e.Gh.def, the doubled shear that gauges it;
• e.recurrence.params (label; display).

What this module supplies

Exactly one input of the factorization ApproximateRecurrence.PrincipalResponseLegsIndep integral_blockQuadratic_shellSplit_eq, namely hW: the second-moment integrability, against M.P.toMeasure, of every product of two doubled coordinates of the gauged load G_{-(h)_{z+cu_n}} P_z. It is the input that ApproximateRecurrence.PrincipalResponseLoadMeas integral_blockQuadratic_shellSplit_eq_gaugedPrincipalLoadShell still carries as a binder.

hW is not supplied unconditionally. It is supplied under the parameter gates the manuscript's own display e.nablaw.in.L.eight is stated under: a threshold gamma0, the induction state S(m0, E), and the three scale gates m - h <= m0, h <= 6 cstar gamma^{-1}, K >= m + 10^10 gamma^{-1} of e.recurrence.params. That is the shape in which the corrector moment exists in this repository at all.

The route, factor by factor

The gauged load is (P_z, -(h)_^{(1)} + P_z^{(2)}). Four quantities enter its squared coordinates, and each is reduced to the volume-normalized Euclidean L^8 norm on the large cube cu_K:

1. the averaged Dirichlet gradient (grad w_D)_R, by the vector Jensen inequality on R and the grid re-assembly descendantsAverage_sq_vecNormSq_add_cubeAverageVec_le read at the single cube R (le_card_mul_descendantsAverage);
2. the averaged flux (grad w_N + shom^{-1} h e')_R, by the same route after the Minkowski step cubeEuclideanLpNorm_add_le;
3. the averaged fresh shell (h)_R, column by column: the j-th column of freshShellCubeAverage is cubeAverageVec R of the field x |-> (k_m - k_n)(x) e_j, i.e. of streamForcing 1 at the direction Pi.single j 1, so the same grid bound applies and cubeEuclideanLpNorm_streamForcing_le converts it to the stream-increment L^8 norm. The passage from the columns to the matrix is the Frobenius bound vecNormSq_matVecMul_le_matrixFrobeniusNormSq_mul_vecNormSq, so no operator-norm-of-an-average estimate is needed;
4. the L^8 membership of the two corrector gradients, which is not a consequence of the H^1 structure and is taken from the frozen external anchor Algsuperdiff.Frozen.External.calderon_zygmund directly: the anchor returns MemLp grad p alongside the norm bound, and Corrector.FreshShellCZ discards the membership.

The two random inputs are then the head-plus-tail displays Corrector.exists_cubeEuclideanL8_gradient_sq_sum_le_const_add_gammaPow (gated; e.nablaw.in.L.eight) and Corrector.exists_streamIncrementLpNormSq_head_tail (ungated; e.km.kn.Lp at p = 8). Neither fluctuation is measurable, so the integrability is obtained through the measurable-proxy device already used by PrincipalResponseDisplayTwoMoment.integral_le_of_le_shift_add_kappa_sq: integrable_of_abs_le_shift_add_kappa_sq below runs CoarseGraining's IndependentSums.integrable_rpow_of_isBigOWith_gammaSigma on sqrt(max(|f| - B, 0)/kappa) and dominates. The two Gamma_1 lanes are merged by isBigOWith_gammaSigma_one_add.

What this module does NOT supply

It does not assemble hindep, and it does not re-state any consumer with hindep removed. hindep remains a binder of ApproximateRecurrence.PrincipalResponseBudgetWire exists_smallCoupling_principalEnergy_bound_of_centering and of its predecessors, untouched by anything below. In particular no declaration below mentions gaugedPrincipalLoadShell_val or any matrix-side declaration of PrincipalResponseLowerShellMeas: the whole file is on the load side of the factorization.

The matrix side of that module is now its representative interface: exists_measurable_representative_switchCubeMatrix produces some B : Cutoff.ShellSeq d → BlockMat d that is entrywise Cutoff.lowerShellLocalCompletion M L U-measurable and agrees with PrincipalResponseIndepWire.switchCubeMatrix almost everywhere under Cutoff.cutoffSampleLaw M, and its consumers carry that pair as binders. An earlier version of this paragraph named the pre-redesign zero-extension surface switchCubeMatrixShell and its _val bridge; those two declarations are private to PrincipalResponseLowerShellMeas, are not part of any interface, and the reference to them is withdrawn here in favour of the representative interface that replaced them.

It supplies no measurability of the load (that is PrincipalResponseLoadMeas.measurable_shellIndexSigma_gaugedPrincipalLoadShell, used here only to obtain the ambient measurability the integrability needs), no moment bound (only finiteness of the second moment is proved; no numerical constant is asserted), and no statement about hBmeas.

Main results

• exists_kappa_abs_gaugedLoad_mul_le -- the pathwise bound; sorry-free.
• exists_gamma0_integrable_toFullBlockVec_gaugedPrincipalLoadShell_mul -- the hW input, under the gates.

References

• ABK26; e.nablaw.in.L.eight (label); e.km.kn.Lp; e.Pz.def (label); e.Gh.def; e.recurrence.params (label).

The L^8 membership of the two corrector gradients

The hW input of the factorization

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.exists_gamma0_integrable_toFullBlockVec_gaugedPrincipalLoadShell_mul (d : ℕ) (hd : 2 ≤ d) : ∃ (gamma0 : ℝ), 0 < gamma0 ∧ gamma0 ≤ 1 / 4 ∧ ∀ (M : ABKModel d), M.gamma ≤ gamma0 → ∀ (m0 : ℤ) (Eind : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M m0 Eind → ∀ (m K : ℤ) (hgap : ℕ), 0 < hgap → m - ↑hgap ≤ m0 → ↑hgap ≤ 6 * Disorder.cstar M * M.gamma⁻¹ → 10 ^ 10 * M.gamma⁻¹ ≤ ↑K - ↑m → ∀ (e e' : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e ≤ 1 → HCPolySupport.Book.Ch02.vecNorm e' ≤ 1 → ∀ (jd : ℕ), ∀ R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d K) jd, ∀ (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d K))) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d K))), (∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) (wD omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑(Annealed.sigmaBar M (m - ↑hgap)))⁻¹ omega (m - ↑hgap) m e x) → (∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) (wN omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑(Annealed.sigmaBar M (m - ↑hgap)))⁻¹ omega (m - ↑hgap) m e' x) → ∀ (alpha beta : HCPolySupport.BlockCoord d), MeasureTheory.Integrable (fun (omega : Cutoff.ShellSeq d) => HCPolySupport.toFullBlockVec (gaugedPrincipalLoadShell (Annealed.sigmaBar M (m - ↑hgap)) R (m - ↑hgap) m e e' wD wN omega) alpha * HCPolySupport.toFullBlockVec (gaugedPrincipalLoadShell (Annealed.sigmaBar M (m - ↑hgap)) R (m - ↑hgap) m e e' wD wN omega) beta) ↑M.P

The second-moment integrability of the gauged load G_{-(h)_R} P_z.

Every product of two doubled coordinates of the gauged load is integrable against M.P.toMeasure. This is the hW input of ApproximateRecurrence.PrincipalResponseLegsIndep integral_blockQuadratic_shellSplit_eq, hence the last integrability binder of ApproximateRecurrence.PrincipalResponseLoadMeas integral_blockQuadratic_shellSplit_eq_gaugedPrincipalLoadShell.

: this statement holds only under the propositions supplied by its binders, which are

• hd -- the paper-wide 2 <= d;
• M.gamma <= gamma0 for the produced threshold, and the induction state Algsuperdiff.Frozen.Section3.inductionState M m0 Eind;
• 0 < hgap, m - hgap <= m0, hgap <= 6 cstar cgamma^{-1} (/7183) and 10^10 cgamma^{-1} <= K - m (e.recurrence.params);
• the two direction bounds vecNorm e <= 1, vecNorm e' <= 1;
• hR, the geometric membership of the localization cube;
• hwD, hwN, the two weak-solution properties of e.def.w (label) for the two families, at every shell sequence.

The first four groups are exactly the gates of e.nablaw.in.L.eight (label); they are inherited, not added, and no numerical bound is asserted: only finiteness of the second moment. It is a provider A, not a source-facing frozen declaration.

Reaches exactly the one permitted frozen theorem Algsuperdiff.Frozen.External.calderon_zygmund (through the L^8 membership of the two corrector gradients and through e.nablaw.in.L.eight), a proved external. The route through e.km.kn.Lp at p = 8 reaches Algsuperdiff.Frozen.Section3.stream_increment_lp_large_cube_bound, also proved.