LocalMeasurability

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

Point values of a shell field are integral-local

The manuscript's local information F(U) is represented on the shell carrier by the integral-generated ShellField.lihLocalSigma U, whose generators are the entry tests j ↦ ∫ j(x)_{ik} φ(x) dx of probes φ supported in U (Algsuperdiff.Assumptions.ShellField.LIHLocalSigma). Every gauge of Section 3.3 — the oscillation gauges localCubeDerivNorm, localCubeSecondDerivNorm of e.BoscL.def in particular — is a supremum of pointwise quantities, so the first thing needed to place those gauges in a local σ-algebra is that a single point value

j ↦ j(x)

is lihLocalSigma U-measurable whenever x is an interior point of U.

This module proves exactly that. No mollification is required: on the shell carrier the value map x ↦ j(x) is continuous by construction, so the closed-ball averages

⨍_{B(x,ρ)} j(y)_{ik} dy

converge to j(x)_{ik} as ρ ↓ 0 for every j (no Lebesgue differentiation, no null set), while each of them is a scalar multiple of the CoarseGraining entry test against the ball indicator — a probe supported in U as soon as the ball is contained in U. A pointwise limit of measurable functions is measurable, which gives the claim.

Main results

• tendsto_setAverage_closedBall: shrinking closed-ball averages of a continuous function converge to its value at the centre.
• measurable_entry_eval_lihLocalSigma: each scalar entry j ↦ j(x)_{ik} is lihLocalSigma U-measurable at every interior point x of U.
• tendsto_diffQuotient_deriv: the difference quotients of the values along a direction converge to the stored first derivative applied to that direction.
• measurable_entry_eval_deriv_lihLocalSigma, measurable_eval_deriv_apply_lihLocalSigma: the directional first derivative j ↦ (∇j)(x)v is lihLocalSigma U-measurable at every interior point x of U. The difference quotients only read values at points of the ball around x already contained in U, so no information outside U is used.

References

• ABK26, sss.bad.cubes (the events whose gauges are pointwise suprema).
• ABK26 (the volume-normalized Sobolev norm entering e.BoscL.def).

Shrinking ball averages of a continuous function

theorem Algsuperdiff.Section3.Provider.BadEvents.tendsto_setAverage_closedBall {d : ℕ} {f : HCPolySupport.Vec d → ℝ} (hf : Continuous f) (x : HCPolySupport.Vec d) {rho : ℕ → ℝ} (hpos : ∀ (n : ℕ), 0 < rho n) (hrho : Filter.Tendsto rho Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ⨍ (y : HCPolySupport.Vec d) in Metric.closedBall x (rho n), f y) Filter.atTop (nhds (f x))

Averages of a continuous real function over closed balls of radii tending to zero converge to its value at the common centre. This is elementary — it uses only that a closed ball has positive finite volume and that the average of a function with values in a closed interval lies in that interval — and in particular it holds at every point, not almost everywhere.

Ball averages of shell entries are integral-local

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_setAverage_entry_lihLocalSigma {d : ℕ} {U : Set (HCPolySupport.Vec d)} {x : HCPolySupport.Vec d} {rho : ℝ} (hrho : Metric.closedBall x rho ⊆ U) (i k : Fin d) : Measurable fun (j : Frozen.Assumptions.ShellField d) => ⨍ (y : HCPolySupport.Vec d) in Metric.closedBall x rho, (↑j).1 y i k

The scalar ball average of a shell entry is a scalar multiple of the CoarseGraining entry test against the ball indicator, hence lihLocalSigma U-measurable as soon as the ball lies in U.

Point values are integral-local

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_entry_eval_lihLocalSigma {d : ℕ} {U : Set (HCPolySupport.Vec d)} {x : HCPolySupport.Vec d} {r : ℝ} (hr : 0 < r) (hrU : Metric.closedBall x r ⊆ U) (i k : Fin d) : Measurable fun (j : Frozen.Assumptions.ShellField d) => (↑j).1 x i k

Each scalar entry of a point value is integral-local. If some closed ball around x lies in U, then j ↦ j(x)_{ik} is measurable for the integral-generated local σ-algebra lihLocalSigma U.

Directional derivatives are integral-local

theorem Algsuperdiff.Section3.Provider.BadEvents.tendsto_diffQuotient_deriv {d : ℕ} (j : Frozen.Assumptions.ShellField d) (x v : HCPolySupport.Vec d) {rho : ℕ → ℝ} (hne : ∀ (n : ℕ), rho n ≠ 0) (hrho : Filter.Tendsto rho Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (rho n)⁻¹ • ((↑j).1 (x + rho n • v) - (↑j).1 x)) Filter.atTop (nhds ((j.deriv x) v))

The difference quotients of the shell values along a direction v converge to the stored derivative applied to v.

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_entry_eval_deriv_lihLocalSigma {d : ℕ} {U : Set (HCPolySupport.Vec d)} {x : HCPolySupport.Vec d} {r : ℝ} (hr : 0 < r) (hrU : Metric.closedBall x r ⊆ U) (v : HCPolySupport.Vec d) (i k : Fin d) : Measurable fun (j : Frozen.Assumptions.ShellField d) => (j.deriv x) v i k

Directional derivatives are integral-local, entrywise. If some closed ball around x lies in U, then j ↦ (∇j)(x)v has lihLocalSigma U-measurable entries.

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_eval_deriv_apply_lihLocalSigma {d : ℕ} {U : Set (HCPolySupport.Vec d)} {x : HCPolySupport.Vec d} {r : ℝ} (hr : 0 < r) (hrU : Metric.closedBall x r ⊆ U) (v : HCPolySupport.Vec d) : Measurable fun (j : Frozen.Assumptions.ShellField d) => (j.deriv x) v

Directional derivatives are integral-local. If some closed ball around x lies in U, then j ↦ (∇j)(x)v is lihLocalSigma U-measurable.