CoefficientMeasurable

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

The coefficient field is a measurable map into the continuous fields on a compact set

On a compact set K the cutoff coefficient field a_m(ω) = ν I + k_m(ω) is a continuous matrix field, and the assignment ω ↦ a_m(ω)|_K is measurable into the Banach space C(K, Mat d) of continuous matrix fields with the supremum norm.

The proof uses no separability argument and no dense evaluation criterion. Each shell of the sample is, by construction, a bundled continuous map, and restriction to K is continuous for the compact-open topologies, so every finite partial sum of shells is a continuous image of finitely many coordinates of the sample and is therefore measurable. The lower-tail control makes the partial sums converge uniformly on every centred cube, hence in C(K, Mat d), and a pointwise limit of measurable maps into a metrizable Borel space is measurable.

Main definitions

• cutoffCoeffMap nu m omega — the coefficient field as a continuous matrix field on ℝ^d.
• coefficientCutoffRestrict nu m K omega — its restriction to K.

Main results

• measurable_coefficientCutoffRestrict — the assignment is measurable.

References

• ABK26, the cutoff coefficient field of Section 3.

Measurability from closed balls

theorem Algsuperdiff.Section5.Support.measurableSet_preimage_isOpen_of_closedBall {Omega : Type u_1} {X : Type u_2} (mOmega : MeasurableSpace Omega) [PseudoMetricSpace X] [TopologicalSpace.SeparableSpace X] {F : Omega → X} (hF : ∀ (c : X) (r : ℝ), MeasurableSet (F ⁻¹' Metric.closedBall c r)) {V : Set X} (hV : IsOpen V) : MeasurableSet (F ⁻¹' V)

In a separable pseudometric space, measurable closed-ball preimages imply measurable open-set preimages.

theorem Algsuperdiff.Section5.Support.measurable_of_preimage_closedBall {Omega : Type u_1} {X : Type u_2} (mOmega : MeasurableSpace Omega) [PseudoMetricSpace X] [TopologicalSpace.SeparableSpace X] [MeasurableSpace X] [BorelSpace X] {F : Omega → X} (hF : ∀ (c : X) (r : ℝ), MeasurableSet (F ⁻¹' Metric.closedBall c r)) : Measurable F

A map into a separable pseudometric Borel space is measurable when its closed-ball preimages are measurable.

Instance caches for Mat d

Mathlib v4.33 assembles the scoped elementwise matrix norm with fast_instance%, so the topology reachable from Matrix.normedAddCommGroup is a flattened copy of the product topology and no longer syntactically the one bare Mat d carries by default (the plain, unconditional TopologicalSpace (Matrix m n R) := inferInstanceAs (TopologicalSpace (m → n → R)) bridging instance). SecondCountableTopology/PseudoMetrizableSpace have no dedicated Matrix-level bridging instance at all, so blind search for them on Mat d fails outright. Both are supplied here, pinned to the same Fin d → Fin d → ℝ spelling the bridging TopologicalSpace instance already uses, so inferInstanceAs closes by unfolding the Matrix type synonym rather than by a fresh (and now-failing) search.

instance Algsuperdiff.Section5.Support.instSecondCountableTopologyMat {d : ℕ} : SecondCountableTopology (HCPolySupport.Mat d)

instance Algsuperdiff.Section5.Support.instPseudoMetrizableSpaceMat {d : ℕ} : TopologicalSpace.PseudoMetrizableSpace (HCPolySupport.Mat d)

@[instance_reducible]

instance Algsuperdiff.Section5.Support.instPseudoMetricSpaceMat {d : ℕ} : PseudoMetricSpace (HCPolySupport.Mat d)

Equations

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

@[instance_reducible]

noncomputable instance Algsuperdiff.Section5.Support.continuousMatrixFieldMeasurableSpace {d : ℕ} (K : Set (HCPolySupport.Vec d)) : MeasurableSpace C(↑K, HCPolySupport.Mat d)

The Borel structure on the continuous matrix fields over a compact carrier.

Equations

• Algsuperdiff.Section5.Support.continuousMatrixFieldMeasurableSpace K = borel C(↑K, HCPolySupport.Mat d)

instance Algsuperdiff.Section5.Support.continuousMatrixFieldBorelSpace {d : ℕ} (K : Set (HCPolySupport.Vec d)) : BorelSpace C(↑K, HCPolySupport.Mat d)

theorem Algsuperdiff.Section5.Support.measurable_continuousMap_of_dense_evaluations {d : ℕ} {Omega : Type u_1} (mOmega : MeasurableSpace Omega) {K : Set (HCPolySupport.Vec d)} [CompactSpace ↑K] {D : Set ↑K} (hDc : D.Countable) (hDd : Dense D) {F : Omega → C(↑K, HCPolySupport.Mat d)} (hF : ∀ z ∈ D, Measurable fun (w : Omega) => (F w) z) : Measurable F

A continuous matrix field on a compact carrier is measurable when its values on a countable dense subset are measurable.

1. Restricting a shell to a compact carrier

def Algsuperdiff.Section5.Support.shellRestrict {d : ℕ} (K : Set (HCPolySupport.Vec d)) (j : Frozen.Assumptions.ShellField d) : C(↑K, HCPolySupport.Mat d)

The restriction of the value part of a shell to a compact carrier.

Equations

• Algsuperdiff.Section5.Support.shellRestrict K j = ContinuousMap.restrict K (↑j).1

theorem Algsuperdiff.Section5.Support.continuous_shellRestrict {d : ℕ} (K : Set (HCPolySupport.Vec d)) : Continuous (shellRestrict K)

theorem Algsuperdiff.Section5.Support.measurable_shellRestrict {d : ℕ} (K : Set (HCPolySupport.Vec d)) : Measurable (shellRestrict K)

2. The coefficient field as a continuous matrix field

noncomputable def Algsuperdiff.Section5.Support.cutoffCoeffMap {d : ℕ} (nu : ℝ) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : C(HCPolySupport.Vec d, HCPolySupport.Mat d)

The cutoff coefficient field at scale m, as a continuous matrix field.

Equations

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

@[simp]

theorem Algsuperdiff.Section5.Support.cutoffCoeffMap_apply {d : ℕ} (nu : ℝ) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (x : HCPolySupport.Vec d) : (cutoffCoeffMap nu m omega) x = (Section3.Cutoff.coefficientCutoff nu m omega).toCoeffField x

noncomputable def Algsuperdiff.Section5.Support.coefficientCutoffRestrict {d : ℕ} (nu : ℝ) (m : ℤ) (K : Set (HCPolySupport.Vec d)) (omega : Section3.Cutoff.CutoffSample d) : C(↑K, HCPolySupport.Mat d)

The coefficient field restricted to a compact carrier.

Equations

• Algsuperdiff.Section5.Support.coefficientCutoffRestrict nu m K omega = ContinuousMap.restrict K (Algsuperdiff.Section5.Support.cutoffCoeffMap nu m omega)

3. Partial sums of shells are measurable

def Algsuperdiff.Section5.Support.shellPartialRestrict {d : ℕ} (K : Set (HCPolySupport.Vec d)) (m : ℤ) (q : ℕ) (omega : Section3.Cutoff.CutoffSample d) : C(↑K, HCPolySupport.Mat d)

The descending partial sum of shells, restricted to a compact carrier.

Equations

• Algsuperdiff.Section5.Support.shellPartialRestrict K m q omega = ∑ r ∈ Finset.range q, Algsuperdiff.Section5.Support.shellRestrict K (↑omega (m - ↑r))

theorem Algsuperdiff.Section5.Support.measurable_shellPartialRestrict {d : ℕ} (K : Set (HCPolySupport.Vec d)) [CompactSpace ↑K] (m : ℤ) (q : ℕ) : Measurable (shellPartialRestrict K m q)

theorem Algsuperdiff.Section5.Support.shellPartialRestrict_apply {d : ℕ} (K : Set (HCPolySupport.Vec d)) (m : ℤ) (q : ℕ) (omega : Section3.Cutoff.CutoffSample d) (x : ↑K) (i j : Fin d) : (shellPartialRestrict K m q omega) x i j = (Section3.Cutoff.finiteLowerCutoff m q ↑omega).toFun (↑x) i j

4. Uniform convergence of the partial sums on a compact carrier

noncomputable def Algsuperdiff.Section5.Support.cutoffMap {d : ℕ} (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : C(HCPolySupport.Vec d, HCPolySupport.Mat d)

The cutoff field as a continuous matrix field.

Equations

• Algsuperdiff.Section5.Support.cutoffMap m omega = { toFun := fun (x : HCPolySupport.Vec d) => (Algsuperdiff.Section3.Cutoff.cutoff m omega).toFun x, continuous_toFun := ⋯ }

noncomputable def Algsuperdiff.Section5.Support.cutoffRestrict {d : ℕ} (K : Set (HCPolySupport.Vec d)) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : C(↑K, HCPolySupport.Mat d)

The cutoff field restricted to a compact carrier.

Equations

• Algsuperdiff.Section5.Support.cutoffRestrict K m omega = ContinuousMap.restrict K (Algsuperdiff.Section5.Support.cutoffMap m omega)

theorem Algsuperdiff.Section5.Support.tendsto_shellPartialRestrict {d : ℕ} (K : Set (HCPolySupport.Vec d)) [CompactSpace ↑K] (m ell : ℤ) (hK : K ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell)) (omega : Section3.Cutoff.CutoffSample d) : Filter.Tendsto (fun (q : ℕ) => shellPartialRestrict K m q omega) Filter.atTop (nhds (cutoffRestrict K m omega))

5. Measurability

theorem Algsuperdiff.Section5.Support.measurable_cutoffRestrict {d : ℕ} (K : Set (HCPolySupport.Vec d)) [CompactSpace ↑K] (m ell : ℤ) (hK : K ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell)) : Measurable (cutoffRestrict K m)

theorem Algsuperdiff.Section5.Support.measurable_coefficientCutoffRestrict {d : ℕ} (nu : ℝ) (K : Set (HCPolySupport.Vec d)) [CompactSpace ↑K] (m ell : ℤ) (hK : K ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell)) : Measurable (coefficientCutoffRestrict nu m K)

The coefficient field is a measurable map into the continuous fields on a compact carrier.