PrincipalResponseLowerShellMeas

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 lower-shell measurability's matrix, at the actual matrix

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.lower.bound.principal.one.pre (label).

What this module supplies

The sentence describes its matrix bfA_{m-h} as built from the shells at or below m - h. In this repository that description is the binder hBmeas of ApproximateRecurrence.PrincipalResponseLegsIndep integral_blockQuadratic_shellSplit_eq, namely

∀ a b : BlockCoord d,
  Measurable[Cutoff.lowerShellLocalCompletion M L U]
    fun omega => blockMatEntry (B omega) a b

and it was carried as a binder by every consumer, at an abstract B. This module supplies it at the concrete matrix that PrincipalResponseSwitchActualPerCube.switchCubeQuad conjugates, i.e. at PrincipalResponseIndepWire.switchCubeMatrix, in two carrier forms:

• measurable_cutoffSampleLocalSigma_blockMatEntry_switchCubeMatrix, on the actual cutoff-sample carrier Cutoff.CutoffSample d, for the local field Cutoff.cutoffSampleLocalSigma M lowScale U of any observation set U containing cubeSet R;
• exists_measurable_representative_switchCubeMatrix, on the shell-sequence carrier Cutoff.ShellSeq d: an existential statement asserting that some function B on that carrier is entrywise Cutoff.lowerShellLocalCompletion M lowScale U-measurable -- literally the hBmeas binder shape -- and agrees with switchCubeMatrix almost everywhere under Cutoff.cutoffSampleLaw M.

The carrier step, disclosed

switchCubeMatrix is a function of Cutoff.CutoffSample d, the lower-tail-good subtype of Cutoff.ShellSeq d, because the genuine lower-infinite cutoff is defined only there. integral_blockQuadratic_shellSplit_eq integrates over (Cutoff.ShellSeq d, M.P.toMeasure). The two are bridged here by an existential representative on the shell-sequence carrier, and by nothing else that a consumer can see.

The witness used inside the proofs is a Function.extend of switchCubeMatrix along Subtype.val, which has to pick some value off the lower-tail-good carrier. That witness and its off-carrier convention are private to this module: no statement exported from this file mentions either, and no exported statement depends on the off-carrier value. What is exported is only the almost-everywhere identification under Cutoff.cutoffSampleLaw M, so the consumer below is quantified over an arbitrary representative and every integral it names is invariant under that identification.

The route

1. Provider.BadEvents.LambdaLocal already carries the coarse-grained energy Mu (cubeSet R) (coefficientCutoff M.nu L omega).toFun and the two diagonal coarse blocks of the actual cutoff as Cutoff.cutoffSampleLocalSigma M L U-measurable functions, for any U with cubeSet R ⊆ U. The two off-diagonal blocks are added here by the same polarization identities (coarseBlockMatrix_upperRight_apply, coarseBlockMatrix_lowerLeft_apply), giving every blockMatEntry of the ambient coarse block matrix of the cutoff on cubeSet R.
2. PrincipalResponseIndepWire.coarseBlockMatrix_cubeSet_coefficientCutoff_eq identifies that ambient matrix with switchCubeMatrix at every sample.
3. The Subtype.val-comap that defines Cutoff.cutoffSampleLocalSigma from Cutoff.lowerShellLocalCompletion is undone set by set, and the resulting preimage is a.e. equal to the upstairs witness because the lower-tail-good carrier is of full measure.
4. The private witness is then discarded from the interface: only its measurability and its almost-everywhere agreement with switchCubeMatrix are exported, as the two components of an existential statement.

What this module does NOT supply

It does not supply hWmeas, hB or hW of integral_blockQuadratic_shellSplit_eq: the consuming statement below carries all three as binders, each visible in its own signature. It also carries the representative itself and both of the representative's properties as binders, so the only input of integral_blockQuadratic_shellSplit_eq that the consumer below discharges is hBbar. No measurability of gaugedSwitchLoad, blockGauge, freshShellCubeAverage or principalPz is asserted or used anywhere below.

It does not remove the independence binder hindep: that binder still stands on ApproximateRecurrence.PrincipalResponseBudgetWire exists_smallCoupling_principalEnergy_bound_of_centering and on its predecessors, untouched by anything here.

Main results

The public surface is three declarations. The zero-extension of switchCubeMatrix along Subtype.val, the lemma computing it on the carrier, and its entrywise measurability are all private, and so is the entrywise expectation transport; none of them is nameable from another module.

• measurable_cutoffSampleLocalSigma_blockMatEntry_switchCubeMatrix
• exists_measurable_representative_switchCubeMatrix
• integral_blockQuadratic_shellSplit_eq_of_representative

References

• ABK26, (the sentence quoted above); e.lower.bound.principal.one.pre (label).

Every entry of the ambient coarse block matrix of the actual cutoff

The exact matrix, on the actual cutoff carrier

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.measurable_cutoffSampleLocalSigma_blockMatEntry_switchCubeMatrix {d : ℕ} [NeZero d] (M : ABKModel d) (lowScale : ℤ) (R : HCPolySupport.TriadicCube d) {U : Set (HCPolySupport.Vec d)} (hRU : HCPolySupport.cubeSet R ⊆ U) (alpha beta : HCPolySupport.BlockCoord d) : Measurable fun (omega : Cutoff.CutoffSample d) => HCPolySupport.blockMatEntry (switchCubeMatrix M lowScale R omega) alpha beta

The lower-shell measurability's matrix, on the cutoff-sample carrier. Every entry of switchCubeMatrix -- the very coarse block matrix that PrincipalResponseSwitchActualPerCube.switchCubeQuad conjugates -- is measurable for the integral-local information at shell index lowScale of any observation set U containing cubeSet R.

: this statement holds under its binders, here the geometric inclusion hRU. It is a provider A, not a source-facing frozen declaration.

The same matrix on the shell-sequence carrier

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.switchCubeMatrixShell {d : ℕ} (M : ABKModel d) (lowScale : ℤ) (R : HCPolySupport.TriadicCube d) : Cutoff.ShellSeq d → HCPolySupport.BlockMat d

Internal. A representative of the matrix on the shell-sequence carrier: switchCubeMatrix extended along Subtype.val by the zero block matrix off the lower-tail-good carrier, on which the genuine lower-infinite cutoff is undefined.

This definition is private, and deliberately so: the zero value off the carrier is a convention with no source content, and no statement exported from this module mentions this definition or depends on that value. The exported interface names only an existential representative and its almost-everywhere agreement with switchCubeMatrix; see exists_measurable_representative_switchCubeMatrix.

Equations

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

The public representative interface

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.exists_measurable_representative_switchCubeMatrix {d : ℕ} [NeZero d] (M : ABKModel d) (lowScale : ℤ) (R : HCPolySupport.TriadicCube d) {U : Set (HCPolySupport.Vec d)} (hRU : HCPolySupport.cubeSet R ⊆ U) : ∃ (B : Cutoff.ShellSeq d → HCPolySupport.BlockMat d), (∀ (alpha beta : HCPolySupport.BlockCoord d), Measurable fun (omega : Cutoff.ShellSeq d) => HCPolySupport.blockMatEntry (B omega) alpha beta) ∧ ∀ᵐ (w : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), B ↑w = switchCubeMatrix M lowScale R w

The hBmeas input of integral_blockQuadratic_shellSplit_eq, at the exact matrix, in representative form.

There is a function B on the shell-sequence carrier Cutoff.ShellSeq d with two properties:

• every entry of B is measurable for Cutoff.lowerShellLocalCompletion M lowScale U, the completed lower-shell local field of any observation set U containing cubeSet R -- this is literally the hBmeas binder shape of ApproximateRecurrence.PrincipalResponseLegsIndep integral_blockQuadratic_shellSplit_eq;
• B agrees with PrincipalResponseIndepWire.switchCubeMatrix almost everywhere under the actual pushforward law Cutoff.cutoffSampleLaw M, i.e. at almost every genuine cutoff sample.

The first property is's description of bfA_{m-h} -- that it is built from the shells at or below m - h -- at the matrix the display actually carries; the second says that the object so described is the display's own matrix, up to a null set of the sample law.

Nothing is asserted about the value of a representative away from the lower-tail-good carrier, and no consumer of this statement can read such a value: the witness produced in the proof is private to this module, and the statement quantifies over B existentially.

: this statement holds under its binders, here the geometric inclusion hRU. It is a provider A, not a source-facing frozen declaration.

The entrywise expectation, transported to the shell carrier

The consumer

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integral_blockQuadratic_shellSplit_eq_of_representative {d : ℕ} [NeZero d] (M : ABKModel d) {L n m : ℤ} (hLn : L ≤ n) {U : Set (HCPolySupport.Vec d)} {K : ℤ} {j : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d K) j) {B : Cutoff.ShellSeq d → HCPolySupport.BlockMat d} (hBmeas : ∀ (alpha beta : HCPolySupport.BlockCoord d), Measurable fun (omega : Cutoff.ShellSeq d) => HCPolySupport.blockMatEntry (B omega) alpha beta) (hBrep : ∀ᵐ (w : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), B ↑w = switchCubeMatrix M L R w) {W : Cutoff.ShellSeq d → HCPolySupport.BlockVec d} (hWmeas : Measurable W) (hB : ∀ (alpha beta : HCPolySupport.BlockCoord d), MeasureTheory.Integrable (fun (omega : Cutoff.ShellSeq d) => HCPolySupport.blockMatEntry (B omega) alpha beta) ↑M.P) (hW : ∀ (alpha beta : HCPolySupport.BlockCoord d), MeasureTheory.Integrable (fun (omega : Cutoff.ShellSeq d) => HCPolySupport.toFullBlockVec (W omega) alpha * HCPolySupport.toFullBlockVec (W omega) beta) ↑M.P) : ∫ (omega : ℤ → Frozen.Assumptions.ShellField d), HCPolySupport.blockVecDot (W omega) (HCPolySupport.blockMatVecMul (B omega) (W omega)) ∂↑M.P = ∫ (omega : ℤ → Frozen.Assumptions.ShellField d), HCPolySupport.blockVecDot (W omega) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M L) ((HCPolySupport.originCube d K).scale - ↑j)) (W omega)) ∂↑M.P

The independence factorization at the exact matrix, with hBbar supplied, at an arbitrary representative.

The matrix is not a concrete term of this file: it is an arbitrary B : Cutoff.ShellSeq d → BlockMat d carrying the two properties that exists_measurable_representative_switchCubeMatrix produces, namely the hBmeas measurability and the almost-everywhere agreement with PrincipalResponseIndepWire.switchCubeMatrix under Cutoff.cutoffSampleLaw M. Both are binders here. Consequently no value of B off the lower-tail-good carrier is read: hBrep enters only through MeasureTheory.integral_congr_ae, and both sides of the conclusion are integrals of B.

Relative to ApproximateRecurrence.PrincipalResponseLegsIndep integral_blockQuadratic_shellSplit_eq, exactly one of the five inputs is gone: hBbar is now PrincipalResponseIndepWire.blockMatEntry_annealedBlockMatrixAtScale_eq_integral_switchCubeMatrix transported to the shell carrier along hBrep, and in its place stands only the geometric membership hR, which also fixes the scale of the annealed matrix to the manuscript's mesoscale (originCube d K).scale - j.

The independence binder hindep of the downstream budget wire is likewise untouched.

: this statement holds only under the propositions supplied by its binders. It is a provider A, not a source-facing frozen declaration.