SupMeasurability

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

The oscillation gauges of e.BoscL.def are integral-local

Algsuperdiff.Section3.Provider.BadEvents.LocalMeasurability places the pointwise data of a shell field — its values and its directional first derivatives — in the integral-generated local sigma-field ShellField.lihLocalSigma U. The gauges of e.BoscL.def are suprema of such pointwise data over the open cube, so two further steps are needed.

• The stored second derivative is recovered from first derivatives by the same difference-quotient limit, and a continuous linear map out of Vec d = Fin d → ℝ is recovered from its values on the standard basis through ContinuousLinearEquiv.piRing. This gives ShellField.secondDeriv j x as a lihLocalSigma U-measurable function of j.
• The supremum over the uncountable open cube is replaced by a supremum over a countable dense subset. This is legitimate because the sharp characterizations unitCubeDerivNorm_le_iff and unitCubeSecondDerivNorm_le_iff' identify the unit-cube norms as the least nonnegative constants dominating a continuous function on the open cube.

The conclusion is that the single-shell oscillation gauge shellOscGauge Q L reads the shell j_L only on the closed cube z + \bar{square}_j: it is measurable for the sigma-field generated by the L-th shell coordinate with its lihLocalSigma-structure on any U containing that closed cube.

Main results

• measurable_eval_deriv_lihLocalSigma, measurable_eval_secondDeriv_lihLocalSigma: the stored derivatives at an interior point are integral-local, as operators.
• unitCubeDerivNorm_eq_iSup, unitCubeSecondDerivNorm_eq_iSup: the unit-cube gauges are countable suprema over a dense subset of the open cube.
• measurable_localCubeDerivNorm_translate_lihLocalSigma, measurable_localCubeSecondDerivNorm_translate_lihLocalSigma: the two L^∞ gauges of the translated shell at scale ell are lihLocalSigma U-measurable whenever U contains the closed ball of radius 3^ell / 2 around the base point, i.e. the closed cube z + \bar{square}_{ell}.
• measurable_shellOscGauge_shellLocal, measurableSet_badOscAt_shellLocal: the e.BoscL.def gauge and event at shell index L are measurable for the L-th shell coordinate's integral-local sigma-field on the closed cube.

References

• ABK26, e.BoscL.def.
• ABK26 (the volume-normalized Sobolev norm).

theorem Algsuperdiff.Section3.Provider.BadEvents.instIsNormableSpaceRealMat (d : ℕ) : IsNormableSpace ℝ (HCPolySupport.Mat d)

theorem Algsuperdiff.Section3.Provider.BadEvents.instIsNormableSpaceRealContinuousLinearMapIdVecMat (d : ℕ) : IsNormableSpace ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Instance caches for the matrix and derivative carriers

Mathlib v4.33 assembles the scoped elementwise matrix norm with fast_instance%, so the topology carried by Matrix.normedAddCommGroup is a flattened copy of the product topology and not the syntactic instTopologicalSpaceMatrix of the ambient Matrix instances; the two agree only once Matrix is unfolded, which instance search will not do. The same splitting happens one level up, where the derivative carrier Vec d →L[ℝ] Mat d is reached both through its operator-norm topology and through the cached one of ShellField.Actions. The declarations below name, once, the MeasurableSpace, BorelSpace and SecondCountableTopology instances that the Measurable API asks for along those paths, in the same spirit as the algebraic caches of ShellField.Actions. Each one is literally the instance Lean would otherwise rediscover.

instance Algsuperdiff.Section3.Provider.BadEvents.instBorelSpaceMatElementwise (d : ℕ) : BorelSpace (HCPolySupport.Mat d)

@[instance_reducible]

noncomputable instance Algsuperdiff.Section3.Provider.BadEvents.instMeasurableSpaceDerivCarrier (d : ℕ) : MeasurableSpace (Frozen.Assumptions.ShellField.MatrixDerivative d)

Equations

• Algsuperdiff.Section3.Provider.BadEvents.instMeasurableSpaceDerivCarrier d = borel (Algsuperdiff.Frozen.Assumptions.ShellField.MatrixDerivative d)

instance Algsuperdiff.Section3.Provider.BadEvents.instBorelSpaceDerivCarrier (d : ℕ) : BorelSpace (Frozen.Assumptions.ShellField.MatrixDerivative d)

instance Algsuperdiff.Section3.Provider.BadEvents.instBorelSpaceDerivCarrierNorm (d : ℕ) : BorelSpace (Frozen.Assumptions.ShellField.MatrixDerivative d)

instance Algsuperdiff.Section3.Provider.BadEvents.instSecondCountableDerivCarrier (d : ℕ) : SecondCountableTopology (Frozen.Assumptions.ShellField.MatrixDerivative d)

@[instance_reducible]

noncomputable instance Algsuperdiff.Section3.Provider.BadEvents.instMeasurableSpaceHessianCarrier (d : ℕ) : MeasurableSpace (Frozen.Assumptions.ShellField.MatrixSecondDerivative d)

Equations

• Algsuperdiff.Section3.Provider.BadEvents.instMeasurableSpaceHessianCarrier d = borel (Algsuperdiff.Frozen.Assumptions.ShellField.MatrixSecondDerivative d)

instance Algsuperdiff.Section3.Provider.BadEvents.instBorelSpaceHessianCarrier (d : ℕ) : BorelSpace (Frozen.Assumptions.ShellField.MatrixSecondDerivative d)

Recovering a continuous linear map from its basis values

The stored first derivative as an operator

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

The stored first derivative is integral-local as an operator. If some closed ball around x lies in U, then j ↦ (∇j)(x) is lihLocalSigma U-measurable with values in Vec d →L[ℝ] Mat d.

The stored second derivative

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

The difference quotients of the stored first derivative along a direction u converge to the stored second derivative applied to u.

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

The stored second derivative is integral-local, entrywise. If some closed ball around x lies in U, then j ↦ (∇²j)(x)uv has lihLocalSigma U-measurable entries.

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

The stored second derivative is integral-local as a matrix value.

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

The stored second derivative is integral-local in the first slot.

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

The stored second derivative is integral-local as an operator.

Countable dense subsets of the open unit cube

theorem Algsuperdiff.Section3.Provider.BadEvents.exists_countable_dense_openCube (d : ℕ) : ∃ (D : Set (HCPolySupport.Vec d)), D.Countable ∧ D ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d 0) ∧ HCPolySupport.openCubeSet (HCPolySupport.originCube d 0) ⊆ closure D

The literal open unit cube of the manuscript carries a countable dense subset, because the ambient space is second countable.

theorem Algsuperdiff.Section3.Provider.BadEvents.unitCubeDerivNorm_eq_iSup {d : ℕ} {D : Set (HCPolySupport.Vec d)} (hDsub : D ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d 0)) (hDdense : HCPolySupport.openCubeSet (HCPolySupport.originCube d 0) ⊆ closure D) (j : Frozen.Assumptions.ShellField d) : j.unitCubeDerivNorm = ⨆ (w : ↑D), Frozen.Assumptions.ShellField.matrixDerivativeNorm (j.deriv ↑w)

The unit-cube first-derivative gauge is a countable supremum.

theorem Algsuperdiff.Section3.Provider.BadEvents.unitCubeSecondDerivNorm_eq_iSup {d : ℕ} {D : Set (HCPolySupport.Vec d)} (hDsub : D ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d 0)) (hDdense : HCPolySupport.openCubeSet (HCPolySupport.originCube d 0) ⊆ closure D) (j : Frozen.Assumptions.ShellField d) : j.unitCubeSecondDerivNorm = ⨆ (w : ↑D), Frozen.Assumptions.ShellField.matrixSecondDerivativeNorm (j.secondDeriv ↑w)

The unit-cube second-derivative gauge is a countable supremum.

The local cube gauges of a translated shell

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_localCubeDerivNorm_translate_lihLocalSigma {d : ℕ} {U : Set (HCPolySupport.Vec d)} (ell : ℤ) (z : HCPolySupport.Vec d) (hU : Metric.closedBall z (1 / 2 * 3 ^ ell) ⊆ U) : Measurable fun (j : Frozen.Assumptions.ShellField d) => Stream.localCubeDerivNorm ell (Frozen.Assumptions.ShellField.translate z j)

The first-derivative cube gauge of a translated shell is integral-local. At scale ell and base point z the gauge reads ∇j only on the closed cube z + \bar{square}_{ell} — the closed ball of radius 3^ell / 2 around z for the ambient sup metric — so any U containing that closed ball suffices.

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_localCubeSecondDerivNorm_translate_lihLocalSigma {d : ℕ} {U : Set (HCPolySupport.Vec d)} (ell : ℤ) (z : HCPolySupport.Vec d) (hU : Metric.closedBall z (1 / 2 * 3 ^ ell) ⊆ U) : Measurable fun (j : Frozen.Assumptions.ShellField d) => Stream.localCubeSecondDerivNorm ell (Frozen.Assumptions.ShellField.translate z j)

The second-derivative cube gauge of a translated shell is integral-local, on the same closed cube.

The e.BoscL.def gauge at a single shell

@[reducible, inline]

abbrev Algsuperdiff.Section3.Provider.BadEvents.shellCoordinateLocalSigma {d : ℕ} (L : ℤ) (U : Set (HCPolySupport.Vec d)) : MeasurableSpace (Cutoff.CutoffSample d)

The sigma-field on the cutoff sample space generated by the integral-local information of the shell of index L in the region U.

Equations

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

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_shellOscGauge_shellLocal {d : ℕ} {U : Set (HCPolySupport.Vec d)} (Q : HCPolySupport.TriadicCube d) (L : ℤ) (hU : Metric.closedBall (cubeBasePoint Q) (1 / 2 * 3 ^ Q.scale) ⊆ U) : Measurable (shellOscGauge Q L)

The single-shell oscillation gauge is local to the closed cube. The gauge 3^{2j} ‖∇ j_L‖_{W^{1,∞}(z + square_j)} of e.BoscL.def reads the shell j_L only on the closed cube z + \bar{square}_j.

theorem Algsuperdiff.Section3.Provider.BadEvents.measurableSet_badOscAt_shellLocal {d : ℕ} {U : Set (HCPolySupport.Vec d)} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (L : ℤ) (hU : Metric.closedBall (cubeBasePoint Q) (1 / 2 * 3 ^ Q.scale) ⊆ U) : MeasurableSet (badOscAt M Q L)

The e.BoscL.def event is local to the closed cube at its own shell.