CutoffMultiscaleEllipticity

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

Measurable multiscale ellipticity of the actual cutoff

The raw quantities below are the Chapter 4 canonical coefficient-family observables of the literal cutoff a_r = nu Id + k_r. On the source range 0 < s, the exported functions are the literal observables clamped at 0; they are genuinely measurable, and they agree with the literals everywhere on the source range, not merely almost everywhere. The positivity proof is a well-definedness input, not a probabilistic or analytic hypothesis: every Section 3 source window already entails it.

Main definitions

• cutoffLowerEllipticityInvLiteral, cutoffUpperEllipticityLiteral: the literal Chapter 4 endpoints at the centered cube.
• cutoffLowerEllipticityInv, cutoffUpperEllipticity: the exported observables, the literals clamped at 0.

Main results

• measurable_cutoffLowerEllipticityInvLiteral, measurable_cutoffUpperEllipticityLiteral: genuine measurability of the literals, from the engine.
• measurable_cutoffLowerEllipticityInv, measurable_cutoffUpperEllipticity.
• cutoffLowerEllipticityInv_nonneg, cutoffUpperEllipticity_nonneg.
• cutoffLowerEllipticityInv_eq_literal, cutoffUpperEllipticity_eq_literal: the exported observable is its literal, at every sample point.
• cutoffLowerEllipticityInv_ae_eq_literal, cutoffUpperEllipticity_ae_eq_literal: the almost-everywhere shadows, kept for the consumers that state their hypotheses that way.

theorem Algsuperdiff.Section3.Observable.neZero_of_model_CutoffMultiscaleEllipticity {d : ℕ} (M : ABKModel d) : NeZero d

noncomputable def Algsuperdiff.Section3.Observable.cutoffLowerEllipticityInvLiteral {d : ℕ} (M : ABKModel d) (domainScale cutoffScale : ℤ) (s : ℝ) (q : CoarseEllipticityExponent) : Cutoff.CutoffSample d → ℝ

Literal inverse lower multiscale ellipticity of the actual cutoff field. This is not selected as a measurable representative.

Equations

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

noncomputable def Algsuperdiff.Section3.Observable.cutoffUpperEllipticityLiteral {d : ℕ} (M : ABKModel d) (domainScale cutoffScale : ℤ) (s : ℝ) (q : CoarseEllipticityExponent) : Cutoff.CutoffSample d → ℝ

Literal upper multiscale ellipticity of the actual cutoff field. This is not selected as a measurable representative.

Equations

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

theorem Algsuperdiff.Section3.Observable.measurable_cutoffLowerEllipticityInvLiteral {d : ℕ} (M : ABKModel d) (domainScale cutoffScale : ℤ) {s : ℝ} (hs : 0 < s) (q : CoarseEllipticityExponent) : Measurable (cutoffLowerEllipticityInvLiteral M domainScale cutoffScale s q)

Genuine measurability of the centered inverse lower multiscale ellipticity literal, from the carrier-source engine at the centered cube.

theorem Algsuperdiff.Section3.Observable.measurable_cutoffUpperEllipticityLiteral {d : ℕ} (M : ABKModel d) (domainScale cutoffScale : ℤ) {s : ℝ} (hs : 0 < s) (q : CoarseEllipticityExponent) : Measurable (cutoffUpperEllipticityLiteral M domainScale cutoffScale s q)

Genuine measurability of the centered upper multiscale ellipticity literal, from the carrier-source engine at the centered cube.

noncomputable def Algsuperdiff.Section3.Observable.cutoffLowerEllipticityInv {d : ℕ} (M : ABKModel d) (domainScale cutoffScale : ℤ) (s : ℝ) (_hs : 0 < s) (q : CoarseEllipticityExponent) : Cutoff.CutoffSample d → ℝ

The actual inverse lower multiscale ellipticity: the literal, clamped at 0.

Equations

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

noncomputable def Algsuperdiff.Section3.Observable.cutoffUpperEllipticity {d : ℕ} (M : ABKModel d) (domainScale cutoffScale : ℤ) (s : ℝ) (_hs : 0 < s) (q : CoarseEllipticityExponent) : Cutoff.CutoffSample d → ℝ

The actual upper multiscale ellipticity: the literal, clamped at 0.

Equations

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

theorem Algsuperdiff.Section3.Observable.measurable_cutoffLowerEllipticityInv {d : ℕ} (M : ABKModel d) (domainScale cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) : Measurable (cutoffLowerEllipticityInv M domainScale cutoffScale s hs q)

theorem Algsuperdiff.Section3.Observable.measurable_cutoffUpperEllipticity {d : ℕ} (M : ABKModel d) (domainScale cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) : Measurable (cutoffUpperEllipticity M domainScale cutoffScale s hs q)

theorem Algsuperdiff.Section3.Observable.cutoffLowerEllipticityInv_nonneg {d : ℕ} (M : ABKModel d) (domainScale cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) (omega : Cutoff.CutoffSample d) : 0 ≤ cutoffLowerEllipticityInv M domainScale cutoffScale s hs q omega

theorem Algsuperdiff.Section3.Observable.cutoffUpperEllipticity_nonneg {d : ℕ} (M : ABKModel d) (domainScale cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) (omega : Cutoff.CutoffSample d) : 0 ≤ cutoffUpperEllipticity M domainScale cutoffScale s hs q omega

theorem Algsuperdiff.Section3.Observable.cutoffLowerEllipticityInv_eq_literal {d : ℕ} (M : ABKModel d) (domainScale cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) : cutoffLowerEllipticityInv M domainScale cutoffScale s hs q = cutoffLowerEllipticityInvLiteral M domainScale cutoffScale s q

The exported inverse lower observable is its literal, at every sample point. This is the payoff of the body swap: the clamp is inert because the literal is nonnegative on the source range 0 < s.

theorem Algsuperdiff.Section3.Observable.cutoffUpperEllipticity_eq_literal {d : ℕ} (M : ABKModel d) (domainScale cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) : cutoffUpperEllipticity M domainScale cutoffScale s hs q = cutoffUpperEllipticityLiteral M domainScale cutoffScale s q

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

theorem Algsuperdiff.Section3.Observable.cutoffLowerEllipticityInv_ae_eq_literal {d : ℕ} (M : ABKModel d) (domainScale cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) : cutoffLowerEllipticityInv M domainScale cutoffScale s hs q =ᵐ[↑(Cutoff.cutoffSampleLaw M)] cutoffLowerEllipticityInvLiteral M domainScale cutoffScale s q

theorem Algsuperdiff.Section3.Observable.cutoffUpperEllipticity_ae_eq_literal {d : ℕ} (M : ABKModel d) (domainScale cutoffScale : ℤ) (s : ℝ) (hs : 0 < s) (q : CoarseEllipticityExponent) : cutoffUpperEllipticity M domainScale cutoffScale s hs q =ᵐ[↑(Cutoff.cutoffSampleLaw M)] cutoffUpperEllipticityLiteral M domainScale cutoffScale s q