CubeEllipticity

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

Multiscale ellipticity of the actual cutoff on an arbitrary triadic cube

Algsuperdiff.Section3.Observable.CutoffMultiscaleEllipticity exposes the measurable Chapter 4 multiscale ellipticity observables of the literal cutoff a_r = nu Id + k_r on the centered cube square_m. ABK26's local bad event e.Bloc.def is stated on the off-centre triadic cube z + square_j for z in 3^j Z^d, i.e. on an arbitrary TriadicCube d of scale j.

The CoarseGraining-only measurability engine used by the centered file (Provider/BadEvents/LiteralMeasurabilityEngine.lean) is already stated for an arbitrary cube, so this module is the verbatim generalization of the centered constructions with originCube d domainScale replaced by a cube parameter. Nothing here is new mathematics; it is the carrier the bad-event definitions need.

Main definitions

• cubeLowerEllipticityInvLiteral, cubeUpperEllipticityLiteral: the literal lambda_{s,q}^{-1}(Q; a_r) and Lambda_{s,q}(Q; a_r).
• cubeLowerEllipticityInv, cubeUpperEllipticity: the exported observables, the literals clamped at 0.

Main results

• measurable_cubeLowerEllipticityInvLiteral, measurable_cubeUpperEllipticityLiteral: genuine measurability of the literals, from the engine.
• measurable_cubeLowerEllipticityInv, measurable_cubeUpperEllipticity
• cubeLowerEllipticityInv_eq_literal, cubeUpperEllipticity_eq_literal: the exported observable is its literal, at every sample point.
• cubeLowerEllipticityInv_ae_eq_literal, cubeUpperEllipticity_ae_eq_literal: the almost-everywhere shadows, kept for the consumers that state their hypotheses that way.
• cubeLowerEllipticityInvLiteral_originCube: on the centered cube the literal observable is the proved centered literal observable. Pointwise centered agreement therefore follows by composing it with the two _eq_literal theorems; no separate transport facade is needed.

References

• ABK26, e.Bloc.def.
• ABK26, (2.22)--(2.23), the coarse-grained ellipticity constants.

theorem Algsuperdiff.Section3.Provider.BadEvents.neZero_of_model {d : ℕ} (M : ABKModel d) : NeZero d

Nonzero dimension, from the paper-wide assumption 2 <= d stored in the model.

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.cubeLowerEllipticityInvLiteral {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (s : ℝ) (q : CoarseEllipticityExponent) : Cutoff.CutoffSample d → ℝ

Literal inverse lower multiscale ellipticity of the actual cutoff field on an arbitrary triadic cube. This is not a measurable representative.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.cubeUpperEllipticityLiteral {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (s : ℝ) (q : CoarseEllipticityExponent) : Cutoff.CutoffSample d → ℝ

Literal upper multiscale ellipticity of the actual cutoff field on an arbitrary triadic cube. This is not a measurable representative.

Equations

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

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_cubeLowerEllipticityInvLiteral {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) {s : ℝ} (hs : 0 < s) (q : CoarseEllipticityExponent) : Measurable (cubeLowerEllipticityInvLiteral M Q cutoffScale s q)

The general-cube inverse lower multiscale ellipticity literal of the actual cutoff is genuinely measurable.

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_cubeUpperEllipticityLiteral {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) {s : ℝ} (hs : 0 < s) (q : CoarseEllipticityExponent) : Measurable (cubeUpperEllipticityLiteral M Q cutoffScale s q)

The general-cube upper multiscale ellipticity literal of the actual cutoff is genuinely measurable.

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.cubeLowerEllipticityInv {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (s : ℝ) (_hs : 0 < s) (q : CoarseEllipticityExponent) : Cutoff.CutoffSample d → ℝ

The actual lambda_{s,q}^{-1}(Q; a_r) on an arbitrary triadic cube: the literal, clamped at 0.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.cubeUpperEllipticity {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (s : ℝ) (_hs : 0 < s) (q : CoarseEllipticityExponent) : Cutoff.CutoffSample d → ℝ

The actual Lambda_{s,q}(Q; a_r) on an arbitrary triadic cube: the literal, clamped at 0.

Equations

• Algsuperdiff.Section3.Provider.BadEvents.cubeUpperEllipticity M Q cutoffScale s _hs q omega = max 0 (Algsuperdiff.Section3.Provider.BadEvents.cubeUpperEllipticityLiteral M Q cutoffScale s q omega)

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_cubeLowerEllipticityInv {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) : Measurable (cubeLowerEllipticityInv M Q cutoffScale s hs q)

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_cubeUpperEllipticity {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) : Measurable (cubeUpperEllipticity M Q cutoffScale s hs q)

theorem Algsuperdiff.Section3.Provider.BadEvents.cubeLowerEllipticityInv_nonneg {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) (omega : Cutoff.CutoffSample d) : 0 ≤ cubeLowerEllipticityInv M Q cutoffScale s hs q omega

theorem Algsuperdiff.Section3.Provider.BadEvents.cubeLowerEllipticityInv_eq_literal {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) : cubeLowerEllipticityInv M Q cutoffScale s hs q = cubeLowerEllipticityInvLiteral M Q cutoffScale s q

The exported general-cube inverse lower observable is its literal, at every sample point. The clamp is inert on the source range 0 < s.

theorem Algsuperdiff.Section3.Provider.BadEvents.cubeUpperEllipticity_eq_literal {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) : cubeUpperEllipticity M Q cutoffScale s hs q = cubeUpperEllipticityLiteral M Q cutoffScale s q

The exported general-cube upper observable is its literal, at every sample point.

theorem Algsuperdiff.Section3.Provider.BadEvents.cubeLowerEllipticityInv_ae_eq_literal {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) : cubeLowerEllipticityInv M Q cutoffScale s hs q =ᵐ[↑(Cutoff.cutoffSampleLaw M)] cubeLowerEllipticityInvLiteral M Q cutoffScale s q

theorem Algsuperdiff.Section3.Provider.BadEvents.cubeUpperEllipticity_ae_eq_literal {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) : cubeUpperEllipticity M Q cutoffScale s hs q =ᵐ[↑(Cutoff.cutoffSampleLaw M)] cubeUpperEllipticityLiteral M Q cutoffScale s q

theorem Algsuperdiff.Section3.Provider.BadEvents.cubeLowerEllipticityInvLiteral_originCube {d : ℕ} (M : ABKModel d) (domainScale cutoffScale : ℤ) (s : ℝ) (q : CoarseEllipticityExponent) : cubeLowerEllipticityInvLiteral M (HCPolySupport.originCube d domainScale) cutoffScale s q = Observable.cutoffLowerEllipticityInvLiteral M domainScale cutoffScale s q

On the centered cube the literal observable is the proved centered literal observable.