Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Cutoff.Limit

Limit #

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

The genuine lower-infinite cutoff #

This file defines the manuscript cutoff only on CutoffSample, the public carrier on which every descending local-control series is summable. Thus the occurrence of tsum below is never used with its nonsummable semantics: the carrier supplies the convergence proof needed at each point and on every origin-centred cube.

The field is built entrywise from the literal series sum_{r >= 0} j_(m-r). Local uniform convergence makes that field continuous, so it is a genuine RegCoeffField; it is not a finite floor or a default value.

source
noncomputable def Algsuperdiff.Section3.Cutoff.cutoffValue {d : ℕ} (m : ℤ) (omega : CutoffSample d) (x : HCPolySupport.Vec d) :
HCPolySupport.Mat d

The matrix-valued lower-infinite shell series at one physical point.

Equations
Instances For
    source
    theorem Algsuperdiff.Section3.Cutoff.continuous_cutoffValue_entry {d : ℕ} (m : ℤ) (omega : CutoffSample d) (i j : Fin d) :
    Continuous fun (x : HCPolySupport.Vec d) => cutoffValue m omega x i j
    source
    noncomputable def Algsuperdiff.Section3.Cutoff.cutoff {d : ℕ} (m : ℤ) (omega : CutoffSample d) :
    HCPolySupport.RegCoeffField d

    The actual lower-infinite cutoff k_m = sum_{n <= m} j_n, defined only on the convergent cutoff carrier.

    Equations
    Instances For
      source
      @[simp]
      theorem Algsuperdiff.Section3.Cutoff.cutoff_apply_entry {d : ℕ} (m : ℤ) (omega : CutoffSample d) (x : HCPolySupport.Vec d) (i j : Fin d) :
      (cutoff m omega).toFun x i j = ∑' (r : ℕ), (↑(↑omega (m - ↑r))).1 x i j
      source
      theorem Algsuperdiff.Section3.Cutoff.continuous_cutoff_entry {d : ℕ} (m : ℤ) (omega : CutoffSample d) (i j : Fin d) :
      Continuous fun (x : HCPolySupport.Vec d) => (cutoff m omega).toFun x i j
      source
      theorem Algsuperdiff.Section3.Cutoff.measurable_cutoff_apply_entry {d : ℕ} (m : ℤ) (x : HCPolySupport.Vec d) (i j : Fin d) :
      Measurable fun (omega : CutoffSample d) => (cutoff m omega).toFun x i j
      source
      theorem Algsuperdiff.Section3.Cutoff.measurable_cutoff {d : ℕ} (m : ℤ) :
      Measurable fun (omega : CutoffSample d) => cutoff m omega

      The lower-infinite cutoff is measurable for CoarseGraining's full regular-field sigma-algebra, including both pointwise and compactly-supported entry-test generators. The entry-test integrals are genuinely integrable by the RegCoeffField carrier; the displayed measurability proof uses their jointly measurable integrands, not a totalized off-carrier series.

      source
      theorem Algsuperdiff.Section3.Cutoff.cutoff_skew {d : ℕ} (m : ℤ) (omega : CutoffSample d) (x : HCPolySupport.Vec d) :
      Matrix.transpose ((cutoff m omega).toFun x) = -(cutoff m omega).toFun x
      source
      theorem Algsuperdiff.Section3.Cutoff.cutoff_add_finiteShellIncrement {d : ℕ} (omega : CutoffSample d) {n m : ℤ} (hnm : n ≤ m) :
      cutoff n omega + finiteShellIncrement (↑omega) n m = cutoff m omega

      The exact finite-increment identity for the lower-infinite cutoffs. This is the carrier equality equivalent to k_m - k_n = sum_(n,m] j_k; phrasing it without subtraction preserves CoarseGraining's additive regular-field carrier.

      source
      theorem Algsuperdiff.Section3.Cutoff.cutoff_sub_cutoff_eq_finiteShellIncrement {d : ℕ} (omega : CutoffSample d) {n m : ℤ} (hnm : n ≤ m) (x : HCPolySupport.Vec d) :
      (cutoff m omega).toFun x - (cutoff n omega).toFun x = (finiteShellIncrement (↑omega) n m).toFun x

      Pointwise subtraction form of the finite-increment identity: k_m - k_n = sum_(n,m] j_k.

      source
      noncomputable def Algsuperdiff.Section3.Cutoff.coefficientCutoff {d : ℕ} (nu : ℝ) (m : ℤ) (omega : CutoffSample d) :
      HCPolySupport.RegCoeffField d

      The coefficient cutoff a_m = nu I + k_m.

      Equations
      Instances For
        source
        @[simp]
        theorem Algsuperdiff.Section3.Cutoff.coefficientCutoff_apply {d : ℕ} (nu : ℝ) (m : ℤ) (omega : CutoffSample d) (x : HCPolySupport.Vec d) :
        (coefficientCutoff nu m omega).toFun x = nu • 1 + (cutoff m omega).toFun x
        source
        theorem Algsuperdiff.Section3.Cutoff.measurable_coefficientCutoff {d : ℕ} (nu : ℝ) (m : ℤ) :
        Measurable fun (omega : CutoffSample d) => coefficientCutoff nu m omega

        The actual coefficient cutoff is measurable for CoarseGraining's full regular-coefficient-field sigma-algebra.

        source
        theorem Algsuperdiff.Section3.Cutoff.symmPart_coefficientCutoff {d : ℕ} (nu : ℝ) (m : ℤ) (omega : CutoffSample d) (x : HCPolySupport.Vec d) :
        HCPolySupport.symmPart ((coefficientCutoff nu m omega).toFun x) = nu • 1

        The symmetric part of the actual coefficient cutoff is exactly nu I. This is a pointwise identity, not an added ellipticity hypothesis.

        source
        theorem Algsuperdiff.Section3.Cutoff.exists_openOriginCube_of_isCompact {d : ℕ} {K : Set (HCPolySupport.Vec d)} (hK : IsCompact K) :
        ∃ (ell : ℤ), K ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell)

        A compact observation region is contained in some open origin cube.