SolutionMeasurable

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

The solution is a measurable function of the sample

The sample enters the localized quantities only through the continuous matrix field a_m(ω) on the closed cube, which is a measurable function of the sample. The integral of the solution over a subset of the cube is a continuous function of that field: subtracting the two weak equations bounds the energy of the difference by the supremum distance of the fields, the zero-trace Poincaré inequality converts the energy into the L² size, and Cauchy-Schwarz against the constant one converts that into the integral. Composing gives measurability in the sample, and the ball-average characterization of a continuous representative turns it into measurability of the pointwise values.

References

• ABK26, the localized error and regularity quantities of Section 5.1.

1. Auxiliary estimates

theorem Algsuperdiff.Section5.Support.abs_setIntegral_le_sqrt {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUfin : MeasureTheory.volume U ≠ ⊤) {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict U)) : |∫ (z : HCPolySupport.Vec d) in U, f z| ≤ √(MeasureTheory.volume.real U) * √(∫ (z : HCPolySupport.Vec d) in U, f z ^ 2)

2. The parameter integral is continuous

noncomputable def Algsuperdiff.Section5.Support.fieldSetIntegral {d : ℕ} (M : Section3.ABKModel d) (y : HCPolySupport.Vec d) (n : ℤ) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Kg : ℝ} (hKg : 0 ≤ Kg) (hg : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) Kg g) (B : Set (HCPolySupport.Vec d)) (A : ↑(ellipticCube M.nu y n)) : ℝ

The integral of the parameter solution over a subset of the cube.

Equations

• Algsuperdiff.Section5.Support.fieldSetIntegral M y n hKg hg B A = ∫ (z : HCPolySupport.Vec d) in B, (Algsuperdiff.Section5.Support.solutionOfField M y n hKg hg A).toFun z

theorem Algsuperdiff.Section5.Support.continuous_fieldSetIntegral {d : ℕ} (M : Section3.ABKModel d) (y : HCPolySupport.Vec d) (n : ℤ) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Kg : ℝ} (hKg : 0 ≤ Kg) (hg : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) Kg g) {B : Set (HCPolySupport.Vec d)} (hBsub : B ⊆ cubeSetAt y n) : Continuous (fieldSetIntegral M y n hKg hg B)

The parameter integral is continuous.

3. Measurability in the sample

theorem Algsuperdiff.Section5.Support.measurable_fieldSetIntegral {d : ℕ} (M : Section3.ABKModel d) (y : HCPolySupport.Vec d) (n : ℤ) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Kg : ℝ} (hKg : 0 ≤ Kg) (hg : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) Kg g) {B : Set (HCPolySupport.Vec d)} (hBsub : B ⊆ cubeSetAt y n) : Measurable (fieldSetIntegral M y n hKg hg B)

theorem Algsuperdiff.Section5.Support.measurable_setIntegral_solutionAt {d : ℕ} (M : Section3.ABKModel d) (m n : ℤ) (y : HCPolySupport.Vec d) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Kg : ℝ} (hKg : 0 ≤ Kg) (hg : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) Kg g) {B : Set (HCPolySupport.Vec d)} (hBsub : B ⊆ cubeSetAt y n) : Measurable fun (omega : Section3.Cutoff.CutoffSample d) => ∫ (z : HCPolySupport.Vec d) in B, (solutionAt M m n y omega hg).toFun z

The integral of the selected solution over a subset of the cube is a measurable function of the sample.