FluxCorrectedTwoScale

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

The two-argument (m, n) flux-corrected error

The carrier layer for the frozen bounds_mathcal_E_aL anchor: the proved one-argument construction of FluxCorrectedRepresentative.lean with the truncation index freed — the (m, n) form of d.mathcal.E at finite q = 2 (the manuscript defines the dropped argument as n := m, which is the _self reduction below, accepted by rfl).

The a.e. identification with CoarseGraining's literal two-argument HomogenizationError at the flux-corrected family is a named provider obligation of bounds_mathcal_E_aL (the matched-index instance is already proved as fluxCorrectedError_ae_eq_representative), not a Support-layer theorem.

neZero_of_model below is a three-line duplicate of the file-private helper in FluxCorrectedRepresentative.lean (and of the public Section3 Orlicz sibling).

theorem Algsuperdiff.Section4.Support.neZero_of_model_FluxCorrectedTwoScale {d : ℕ} (M : Section3.ABKModel d) : NeZero d

noncomputable def Algsuperdiff.Section4.Support.fluxCorrectedTwoScaleErrorFunctional {d : ℕ} (M : Section3.ABKModel d) (L m n : ℤ) (s : ℝ) : Section3.Cutoff.CutoffSample d → ℝ

The two-argument (m, n) flux-corrected (∞,2) error functional.

Equations

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

theorem Algsuperdiff.Section4.Support.fluxCorrectedTwoScaleErrorFunctional_nonneg {d : ℕ} (M : Section3.ABKModel d) (L m n : ℤ) (s : ℝ) (omega : Section3.Cutoff.CutoffSample d) : 0 ≤ fluxCorrectedTwoScaleErrorFunctional M L m n s omega

theorem Algsuperdiff.Section4.Support.measurable_fluxCorrectedTwoScaleErrorFunctional {d : ℕ} (M : Section3.ABKModel d) (L : ℤ) {m n : ℤ} (hnm : n ≤ m) {s : ℝ} : Measurable (fluxCorrectedTwoScaleErrorFunctional M L m n s)

noncomputable def Algsuperdiff.Section4.Support.fluxCorrectedTwoScaleErrorRepresentative {d : ℕ} (M : Section3.ABKModel d) (L m n : ℤ) (s : { s : ℝ // 0 < s }) : Section3.Cutoff.CutoffSample d → ℝ

The two-argument representative at the {s // 0 < s} public carrier.

Equations

• Algsuperdiff.Section4.Support.fluxCorrectedTwoScaleErrorRepresentative M L m n s = Algsuperdiff.Section4.Support.fluxCorrectedTwoScaleErrorFunctional M L m n ↑s

theorem Algsuperdiff.Section4.Support.measurable_fluxCorrectedTwoScaleErrorRepresentative {d : ℕ} (M : Section3.ABKModel d) (L : ℤ) {m n : ℤ} (hnm : n ≤ m) (s : { s : ℝ // 0 < s }) : Measurable (fluxCorrectedTwoScaleErrorRepresentative M L m n s)

noncomputable def Algsuperdiff.Section4.Support.fluxCorrectedTwoScaleErrorObservableSup {d : ℕ} (M : Section3.ABKModel d) (m n : ℤ) (s : { s : ℝ // 0 < s }) : Section3.Cutoff.CutoffSample d → ENNReal

The two-argument sup_{L ≥ m} observable, taken in [0,∞] so no convergence side condition enters the statement.

Equations

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

theorem Algsuperdiff.Section4.Support.measurable_fluxCorrectedTwoScaleErrorObservableSup {d : ℕ} (M : Section3.ABKModel d) {m n : ℤ} (hnm : n ≤ m) (s : { s : ℝ // 0 < s }) : Measurable (fluxCorrectedTwoScaleErrorObservableSup M m n s)

theorem Algsuperdiff.Section4.Support.le_fluxCorrectedTwoScaleErrorObservableSup {d : ℕ} (M : Section3.ABKModel d) (m n : ℤ) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) {L : ℤ} (hL : m ≤ L) : ENNReal.ofReal (fluxCorrectedTwoScaleErrorRepresentative M L m n s omega) ≤ fluxCorrectedTwoScaleErrorObservableSup M m n s omega