CutoffResponseJ

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

The Section 3 cutoff response observable

This module defines the source-facing Section 3.5 response observable using the genuine running diffusivity sigmaBar at the coefficient-cutoff scale. It evaluates the single measurable representative of the entire coarse block, so every direction shares one probability-one event.

The final common-event theorem identifies this measurable observable with the literal manuscript expression J(square_m, sigmaBar_L^(-1/2)e, sigmaBar_L^(1/2)e; a_L) simultaneously for every direction e. No direction-dependent measurable modification and no fallback comparator enters the definition.

References

• ABK26, (2.4), definition of J(U,p,q;a).
• ABK26, Section 3.5, Proposition p.homogenization.step.

noncomputable def Algsuperdiff.Section3.Observable.cutoffResponseJ {d : ℕ} (M : ABKModel d) (cubeScale coefficientScale : ℤ) (e : HCPolySupport.Vec d) : Cutoff.CutoffSample d → ℝ

The measurable Section 3.5 response at cube scale m, coefficient-cutoff scale L, and direction e, with the comparator fixed to the genuine running diffusivity sigmaBar_L. It is evaluated from the one common full coarse-block representative.

Equations

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

theorem Algsuperdiff.Section3.Observable.measurable_cutoffResponseJ {d : ℕ} (M : ABKModel d) (cubeScale coefficientScale : ℤ) (e : HCPolySupport.Vec d) : Measurable (cutoffResponseJ M cubeScale coefficientScale e)

For each direction, the source-facing cutoff response is measurable under the genuine cutoff-sample law.

theorem Algsuperdiff.Section3.Observable.ae_forall_cutoffResponseJ_eq_literal {d : ℕ} (M : ABKModel d) (cubeScale coefficientScale : ℤ) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (e : HCPolySupport.Vec d), cutoffResponseJ M cubeScale coefficientScale e omega = HCPolySupport.ResponseJ (HCPolySupport.cubeSet (HCPolySupport.originCube d cubeScale)) (inverseSqrtLoad (Annealed.sigmaBar M coefficientScale) e) (sqrtLoad (Annealed.sigmaBar M coefficientScale) e) (Cutoff.coefficientCutoff M.nu coefficientScale omega).toFun

On one probability-one event, simultaneously for every direction, the measurable source-facing response is exactly the literal manuscript quantity J(square_m, sigmaBar_L^(-1/2)e, sigmaBar_L^(1/2)e; a_L).

theorem Algsuperdiff.Section3.Observable.ae_forall_coefficientScale_cutoffResponseJ_eq_literal {d : ℕ} (M : ABKModel d) (cubeScale : ℤ) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (coefficientScale : ℤ) (e : HCPolySupport.Vec d), cutoffResponseJ M cubeScale coefficientScale e omega = HCPolySupport.ResponseJ (HCPolySupport.cubeSet (HCPolySupport.originCube d cubeScale)) (inverseSqrtLoad (Annealed.sigmaBar M coefficientScale) e) (sqrtLoad (Annealed.sigmaBar M coefficientScale) e) (Cutoff.coefficientCutoff M.nu coefficientScale omega).toFun

At each fixed cube scale, one probability-one event identifies the entire integer-indexed family of source-facing responses with the literal manuscript family, simultaneously for every coefficient-cutoff scale L and every direction e. Countability is used only for the intersection over L; the uncountable direction quantifier was already placed inside each fixed-L event by the common full-block representative.

theorem Algsuperdiff.Section3.Observable.ae_forall_cutoffResponseJ_nonneg {d : ℕ} (M : ABKModel d) (cubeScale coefficientScale : ℤ) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (e : HCPolySupport.Vec d), 0 ≤ cutoffResponseJ M cubeScale coefficientScale e omega

The source-facing response is nonnegative simultaneously in every direction on one probability-one event. Pointwise nonnegativity off that event is neither asserted nor needed for the measurable representative.