CoefficientLocalMeasurable

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

The coefficient field on a closed cube is a local observable

The local information carried by a region is generated by the integrals of the entries of the coefficient field against test functions supported in that region. It is therefore an integral notion, while the solution of a Dirichlet problem on the cube is built from the field on the cube, an element of the Banach space of continuous matrix fields on the closed cube. This module bridges the two.

Two elementary steps do it. First, the value of a continuous field at a point is the limit of its averages over closed balls shrinking to that point, and each such average is a scalar multiple of the integral of an entry against the indicator of the ball, hence a local observable as soon as the ball lies in the region. Second, a map into the continuous fields on a compact carrier is Borel measurable as soon as its values at the points of a countable dense subset of the carrier are measurable: the distance to a fixed field is the supremum of the pointwise distances over that subset, so the preimage of every closed ball is measurable, and in a separable metric space the closed balls generate the Borel sets.

Applied to y + □_n the two steps give the conclusion for the local information of the closed cube itself: the points of the open cube are dense in the closed cube, and around each of them a closed ball still fits inside the cube, so no enlargement of the region is needed.

Main results

• closedCubeAt_subset_closure_cubeSetAt — the closed cube is the closure of the open cube.
• measurable_coefficientCutoff_apply_local — the value of the coefficient field at a point interior to the region is a local observable.
• measurable_coefficientCutoffRestrict_local — the coefficient field on the closed cube is a local observable of the closed cube.

References

• ABK26, the cutoff coefficient field of Section 3 and the localized Dirichlet problems of Section 5.1.

2. Measurability into the continuous fields on a compact carrier

3. The closed cube is the closure of the open cube

theorem Algsuperdiff.Section5.Support.closedCubeAt_subset_closure_cubeSetAt {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : closedCubeAt y n ⊆ closure (cubeSetAt y n)

The closed cube is the closure of the open cube. Contracting a point of the closed cube towards the centre lands in the open cube and moves it as little as one likes.

4. Local measurability of the values of the coefficient field

theorem Algsuperdiff.Section5.Support.measurable_coefficientCutoff_apply_local {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (U : Set (HCPolySupport.Vec d)) {z : HCPolySupport.Vec d} {rho : ℝ} (hrho : 0 < rho) (hball : Metric.closedBall z rho ⊆ U) : Measurable fun (omega : Section3.Cutoff.CutoffSample d) => (Section3.Cutoff.coefficientCutoff M.nu m omega).toFun z

The value of the coefficient field at a point is a local observable. Around a point at positive distance from the complement of the local set the field is the limit of its averages over shrinking closed balls, and each such average is a scalar multiple of a supported integral test.

5. The coefficient field on the closed cube

theorem Algsuperdiff.Section5.Support.measurable_coefficientCutoffRestrict_local {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (y : HCPolySupport.Vec d) (n : ℤ) : Measurable (coefficientCutoffRestrict M.nu m (closedCubeAt y n))

The coefficient field restricted to the closed cube is measurable for the local information of the closed cube. Its values at the points of the open cube are limits of averages over closed balls contained in the cube, and those points are dense in the closed cube.