InteriorRebase

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

The child frame, re-based on the parent's antisymmetric flux increment

The child-frame composition takes the coarse-graining estimate at the child's own flux-corrected family ã_{L,n} — the cutoff coefficient at the translated sample translateCutoffSample x ω minus the child's own increment (κ_L − κ_n)_{□_n}.

This module supplies the re-basing. The two families differ by a constant antisymmetric matrix, so the equation does not see the difference:

  ã_{L,n}(·, ω_x)  −  ã_{L,n+2}(· + (x−z), ω_z)  =  (κ_L−κ_{n+2})_{□_{n+2}}(ω_z)
                                                  − (κ_L−κ_n)_{□_n}(ω_x) ,

both increments skew. Rather than compare the two, the family below is built directly at the parent's constant, from the proved free-constant carrier Provider.Annular.subConstCutoffTriadicCoeffFamily — so its representative is literally

  a_L(·, translateCutoffSample x ω) − (κ_L−κ_{n+2})_{□_{n+2}}(translateCutoffSample z ω)
      =  ã_{L,n+2}(· + (x−z), translateCutoffSample z ω) ,

which is exactly the hypothesis InteriorGlueFrame consumes: the family's representative is translateCoeffField (x−z) of the parent's carrier field, on every cube. Both facts below are identities; no estimate is made.

References

• ABK26, l.harmonic.approximation.good.scales, (the "differ by a constant anti-symmetric matrix" observation).

1. The parent's constant

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.parentFluxIncrement {d : ℕ} (M : Section3.ABKModel d) (L k : ℤ) (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : HCPolySupport.Mat d

The parent cube's averaged flux increment (κ_L − κ_{n+2})_{□_{n+2}}, read at the anchor's own translated sample translateCutoffSample z ω.

Equations

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.matTranspose_parentFluxIncrement {d : ℕ} (M : Section3.ABKModel d) (L k : ℤ) (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : HCPolySupport.matTranspose (parentFluxIncrement M L k z omega) = -parentFluxIncrement M L k z omega

The parent's increment is antisymmetric (a.shell.antisymmetry).

2. The re-based child-frame family

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.parentRebasedFamily {d : ℕ} (M : Section3.ABKModel d) (L k : ℤ) (x z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : HCPolySupport.Book.Ch03.CoeffFamily d

The child-frame coefficient family at the parent's flux correction.

The cutoff coefficient at the child's translated sample, minus the parent's antisymmetric increment. Built from the proved free-constant carrier, so it is a genuine Ch03.CoeffFamily with the same representative on every cube.

Equations

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

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.parentRebasedFamily_coeffOn {d : ℕ} (M : Section3.ABKModel d) (L k : ℤ) (x z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) (Q : HCPolySupport.TriadicCube d) : ((parentRebasedFamily M L k x z omega).coeffOn Q).toCoeffField = Annular.subConstCutoffField M L (parentFluxIncrement M L k z omega) (Section3.Cutoff.translateCutoffSample x omega)

3. The frame identity

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coefficientCutoff_translate_sub {d : ℕ} (M : Section3.ABKModel d) (L : ℤ) (x z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) (y : HCPolySupport.Vec d) : (Section3.Cutoff.coefficientCutoff M.nu L (Section3.Cutoff.translateCutoffSample z omega)).toCoeffField (y + (x - z)) = (Section3.Cutoff.coefficientCutoff M.nu L (Section3.Cutoff.translateCutoffSample x omega)).toCoeffField y

The cutoff coefficient at the child's translated sample is the cutoff coefficient at the parent's, moved by x − z.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.parentRebasedFamily_coeffOn_eq_translateCoeffField {d : ℕ} (M : Section3.ABKModel d) (L k : ℤ) (x z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) (Q : HCPolySupport.TriadicCube d) : ((parentRebasedFamily M L k x z omega).coeffOn Q).toCoeffField = HCPolySupport.translateCoeffField (x - z) (Support.fluxCorrectedRegField M L k (HCPolySupport.originCube d k) (Section3.Cutoff.translateCutoffSample z omega)).toFun

The frame identity.

The re-based family's representative is, on every cube, the x−z translate of the parent's flux-corrected carrier field at the parent's translated sample.

4. The equation at the re-based family

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isForcedEquation_parentRebasedFamily {d : ℕ} {n m k : ℤ} (M : Section3.ABKModel d) (L : ℤ) (x z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) {u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hsub : HCPolySupport.translateSet x (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (heq : Support.IsDivFormWeakSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u g) : HCPolySupport.Book.Ch03.IsForcedEquation (HCPolySupport.originCube d n) (parentRebasedFamily M L k x z omega) (HCPolySupport.H1Function.untranslate x (u.restrict ⋯ hsub)) fun (y : HCPolySupport.Vec d) => -g (y + x)

The anchor's equation, in the child's frame at the parent's correction.

Restriction to x + □_n, untranslation to the child's own frame, and the antisymmetric shift by the parent's constant, composed.