SplitProducerLoad

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

The Step-2 principal load is sample-measurable on the cutoff carrier

ABK26, l.approximate.recurrence.formula, Step 2, e.Pz.def.

What this module supplies

LocalizationFluctuationMuMeasCell.integrable_switchCubeEnergy_of_le --- the producer of the hintPrincipal binder of integral_blockVecDot_recurrenceP_le_principalSwitchEnergyAverage_add --- carries two inputs: measurability of the load family, and an almost-sure integrable upper bound for the switch energy. This module supplies the first one at the endpoint's own load and on the endpoint's own carrier Cutoff.CutoffSample d.

PrincipalResponseLoadMeas.measurable_shellIndexSigma_principalPz proves the statement on Cutoff.ShellSeq d for the sub-sigma-field generated by the fresh shells (n, m]. Two transports finish it: Cutoff.shellIndexSigma_le_borel turns the fresh-block measurability into plain measurability, and measurable_subtype_coe moves the carrier to the lower-tail-good subtype the Step-2 endpoint integrates over.

The second input --- the almost-sure integrable upper bound --- is not supplied here and is not implied by anything below.

Binders

Beyond the typing binders: [NeZero d], the geometric membership of the localization cube in the mesh below the large cube, and the two weak-solution properties of e.def.w for the corrector families. No measurability, continuity or selection property of the families is assumed, and no estimate, moment or smallness occurs.

Scope

There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.

References

• ABK26, l.approximate.recurrence.formula, Step 2, e.Pz.def, e.def.w.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.measurable_principalPz_shellSeq {d : ℕ} [NeZero d] {Q R : HCPolySupport.TriadicCube d} {jd : ℕ} (hR : R ∈ HCPolySupport.descendantsAtDepth Q jd) (sigma : Observable.PositiveScalar) (sigmaInvD sigmaInvN : ℝ) (n m : ℤ) (eD eN e e' : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) (hwD : ∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) (wD omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing sigmaInvD omega n m eD x) (hwN : ∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) (wN omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing sigmaInvN omega n m eN x) : Measurable fun (omega : Cutoff.ShellSeq d) => principalPz sigma omega n m e e' R (wD omega) (wN omega)

e.Pz.def's load is measurable in the sample, on the shell carrier. The fresh-block statement of PrincipalResponseLoadMeas, read against the full sigma-field.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.measurable_principalPz_cutoffSample {d : ℕ} [NeZero d] {Q R : HCPolySupport.TriadicCube d} {jd : ℕ} (hR : R ∈ HCPolySupport.descendantsAtDepth Q jd) (sigma : Observable.PositiveScalar) (sigmaInvD sigmaInvN : ℝ) (n m : ℤ) (eD eN e e' : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) (hwD : ∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) (wD omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing sigmaInvD omega n m eD x) (hwN : ∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) (wN omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing sigmaInvN omega n m eN x) : Measurable fun (omega : Cutoff.CutoffSample d) => principalPz sigma (↑omega) n m e e' R (wD ↑omega) (wN ↑omega)

The hmeas input of LocalizationFluctuationMuMeasCell.integrable_switchCubeEnergy_descendants, at the endpoint's own carrier.

only on the geometric membership of the cell and the two weak-solution properties of e.def.w.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.measurable_meshCellLoad {d : ℕ} [NeZero d] (M : ABKModel d) (n : ℤ) (h : ℕ) (Kc : ℤ) (e e' : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (hwD : ∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc)) (wD omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑(Annealed.sigmaBar M n))⁻¹ omega n (n + ↑h) e x) (hwN : ∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc)) (wN omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑(Annealed.sigmaBar M n))⁻¹ omega n (n + ↑h) e' x) {jd : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d Kc) jd) : Measurable (meshCellLoad M n h Kc e e' wD wN R)

The same, at the name LocalizationFluctuationMuMeasCell.meshCellLoad gives the load. Definitional.