CoefficientFamily

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

The genuine triadic coefficient family of a cutoff

Every cube receives the same literal coefficient representative a_m = nu I + k_m. Its local upper ellipticity constant is selected from a proved compact-cube bound of that continuous representative; compatibility is therefore pointwise, not an additional assumption or a chosen off-cube extension.

theorem Algsuperdiff.Section3.Cutoff.exists_nat_openOriginCube_of_isCompact {d : ℕ} {K : Set (HCPolySupport.Vec d)} (hK : IsCompact K) : ∃ (n : ℕ), K ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑n)

Every compact set in this finite-dimensional ambient space lies in an open origin cube at a nonnegative integer scale.

noncomputable def Algsuperdiff.Section3.Cutoff.cubeOriginCoverDepth {d : ℕ} (Q : HCPolySupport.TriadicCube d) : ℕ

The least nonnegative origin-cube scale whose open cube contains the closure of Q. This canonical depth is geometric data of Q, not a chosen ellipticity witness.

Equations

• Algsuperdiff.Section3.Cutoff.cubeOriginCoverDepth Q = Nat.find ⋯

noncomputable def Algsuperdiff.Section3.Cutoff.cubeOriginCoverScale {d : ℕ} (Q : HCPolySupport.TriadicCube d) : ℤ

The canonical integer scale associated to cubeOriginCoverDepth.

Equations

• Algsuperdiff.Section3.Cutoff.cubeOriginCoverScale Q = ↑(Algsuperdiff.Section3.Cutoff.cubeOriginCoverDepth Q)

theorem Algsuperdiff.Section3.Cutoff.closure_subset_originCover {d : ℕ} (Q : HCPolySupport.TriadicCube d) : closure (HCPolySupport.openCubeSet Q) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d (cubeOriginCoverScale Q))

theorem Algsuperdiff.Section3.Cutoff.cubeOriginCoverDepth_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (n : ℕ) (hn : closure (HCPolySupport.openCubeSet Q) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑n)) : cubeOriginCoverDepth Q ≤ n

Minimality makes the enclosing origin scale canonical, rather than an arbitrary compactness choice.

theorem Algsuperdiff.Section3.Cutoff.openCubeSet_subset_originCover {d : ℕ} (Q : HCPolySupport.TriadicCube d) : HCPolySupport.openCubeSet Q ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d (cubeOriginCoverScale Q))

noncomputable def Algsuperdiff.Section3.Cutoff.coefficientCutoffCubeEntryBound {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) (Q : HCPolySupport.TriadicCube d) : ℝ

The measurable, sample-dependent entry envelope used by the actual coefficient on Q. It is the molecular constant plus the genuine lower-tail local control on a deterministic enclosing origin cube.

Equations

• Algsuperdiff.Section3.Cutoff.coefficientCutoffCubeEntryBound M m omega Q = M.nu + Algsuperdiff.Section3.Cutoff.cutoffLocalControl (Algsuperdiff.Section3.Cutoff.cubeOriginCoverScale Q) m omega

theorem Algsuperdiff.Section3.Cutoff.measurable_coefficientCutoffCubeEntryBound {d : ℕ} (M : ABKModel d) (m : ℤ) (Q : HCPolySupport.TriadicCube d) : Measurable fun (omega : CutoffSample d) => coefficientCutoffCubeEntryBound M m omega Q

theorem Algsuperdiff.Section3.Cutoff.abs_coefficientCutoff_entry_le_cubeEntryBound {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) (Q : HCPolySupport.TriadicCube d) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet Q) (i j : Fin d) : |(coefficientCutoff M.nu m omega).toFun x i j| ≤ coefficientCutoffCubeEntryBound M m omega Q

noncomputable def Algsuperdiff.Section3.Cutoff.coefficientCutoffCubeEllipticityUpper {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) (Q : HCPolySupport.TriadicCube d) : ℝ

The actual upper ellipticity constant on one triadic cube. Its dependence on the realised cutoff control is retained explicitly; only the lower leg is the molecular diffusivity.

Equations

• Algsuperdiff.Section3.Cutoff.coefficientCutoffCubeEllipticityUpper M m omega Q = (↑d * ↑d * Algsuperdiff.Section3.Cutoff.coefficientCutoffCubeEntryBound M m omega Q ^ 2 + M.nu ^ 2) / M.nu

theorem Algsuperdiff.Section3.Cutoff.measurable_coefficientCutoffCubeEllipticityUpper {d : ℕ} (M : ABKModel d) (m : ℤ) (Q : HCPolySupport.TriadicCube d) : Measurable fun (omega : CutoffSample d) => coefficientCutoffCubeEllipticityUpper M m omega Q

The chosen upper ellipticity constant is measurable in the genuine cutoff sample. Its geometric cover is canonical and its random part is precisely the measurable lower-tail control.

theorem Algsuperdiff.Section3.Cutoff.isEllipticFieldOn_coefficientCutoff_cube {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.IsEllipticFieldOn M.nu (coefficientCutoffCubeEllipticityUpper M m omega Q) (HCPolySupport.openCubeSet Q) (coefficientCutoff M.nu m omega).toFun

noncomputable def Algsuperdiff.Section3.Cutoff.coefficientCutoffCoeffOn {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain Q)

The literal Chapter 2 coefficient object of the actual cutoff on one triadic cube.

Equations

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

@[simp]

theorem Algsuperdiff.Section3.Cutoff.coefficientCutoffCoeffOn_toCoeffField {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) (Q : HCPolySupport.TriadicCube d) : (coefficientCutoffCoeffOn M m omega Q).toCoeffField = (coefficientCutoff M.nu m omega).toFun

noncomputable def Algsuperdiff.Section3.Cutoff.coefficientCutoffTriadicCoeffFamily {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) : HCPolySupport.Book.Ch02.TriadicCoeffFamily d

The compatible triadic family associated to the genuine cutoff. Every cube uses the same pointwise coefficient field; only its locally derived ellipticity witness changes with the cube.

Equations

• Algsuperdiff.Section3.Cutoff.coefficientCutoffTriadicCoeffFamily M m omega = { coeffOn := Algsuperdiff.Section3.Cutoff.coefficientCutoffCoeffOn M m omega, restrictsTo_of_subset := ⋯ }

theorem Algsuperdiff.Section3.Cutoff.coefficientCutoffTriadicCoeffFamily_coeffOn_aeeq {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) (Q : HCPolySupport.TriadicCube d) : ((coefficientCutoffTriadicCoeffFamily M m omega).coeffOn Q).AEEq (coefficientCutoffCoeffOn M m omega Q)