ReplacementDatum

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

The coarse-graining datum, populated

Nothing here imports that file, and nothing here claims the anchor or any source node.

References

• ABK26, l.harmonic.approximation.good.scales.

1. The populated datum

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.coarseGrainingDatum {d : ℕ} [NeZero d] {Q : HCPolySupport.TriadicCube d} (a : HCPolySupport.Book.Ch03.CoeffFamily d) (a0 : HCPolySupport.Book.Ch03.ConstantCoeffMatrix d) {u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : HCPolySupport.Book.Ch03.IsForcedEquation Q a u g) (hg : HCPolySupport.MemVectorL2 (HCPolySupport.openCubeSet Q) g) : HCPolySupport.Book.Ch03.CoarseGrainingComparisonDatum Q a a0 g

The coarse-graining comparison datum, constructed.

u is the given solution of −∇·a∇u = ∇·g; v is the auxiliary constant-coefficient solution v_g; the zero-trace difference is the chosen corrector, and the identity u − v_g = ρ_g holds pointwise.

Equations

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

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coarseGrainingDatum_u {d : ℕ} [NeZero d] {Q : HCPolySupport.TriadicCube d} (a : HCPolySupport.Book.Ch03.CoeffFamily d) (a0 : HCPolySupport.Book.Ch03.ConstantCoeffMatrix d) {u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : HCPolySupport.Book.Ch03.IsForcedEquation Q a u g) (hg : HCPolySupport.MemVectorL2 (HCPolySupport.openCubeSet Q) g) : (coarseGrainingDatum a a0 hu hg).u = u

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coarseGrainingDatum_v {d : ℕ} [NeZero d] {Q : HCPolySupport.TriadicCube d} (a : HCPolySupport.Book.Ch03.CoeffFamily d) (a0 : HCPolySupport.Book.Ch03.ConstantCoeffMatrix d) {u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : HCPolySupport.Book.Ch03.IsForcedEquation Q a u g) (hg : HCPolySupport.MemVectorL2 (HCPolySupport.openCubeSet Q) g) : (coarseGrainingDatum a a0 hu hg).v = forcedReplacement a0 u hg

2. The H¹₀ test function on the half-open cube

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.replacementDefect {d : ℕ} [NeZero d] {Q : HCPolySupport.TriadicCube d} (a0 : HCPolySupport.Book.Ch03.ConstantCoeffMatrix d) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : HCPolySupport.MemVectorL2 (HCPolySupport.openCubeSet Q) g) : HCPolySupport.H10Function (HCPolySupport.cubeSet Q)

The chosen corrector, transported to the half-open cube: the H¹₀ function whose value is u − v_g and whose gradient is ∇u − ∇v_g.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.replacementDefect a0 u hg = (Algsuperdiff.Section4.Provider.ExcessDecay.dirichletCorrector a0 u hg).toCubeSet

theorem Algsuperdiff.Section4.Provider.ExcessDecay.replacementDefect_grad {d : ℕ} [NeZero d] {Q : HCPolySupport.TriadicCube d} (a : HCPolySupport.Book.Ch03.CoeffFamily d) (a0 : HCPolySupport.Book.Ch03.ConstantCoeffMatrix d) {u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : HCPolySupport.Book.Ch03.IsForcedEquation Q a u g) (hg : HCPolySupport.MemVectorL2 (HCPolySupport.openCubeSet Q) g) (x : HCPolySupport.Vec d) : (replacementDefect a0 u hg).grad x = (coarseGrainingDatum a a0 hu hg).u.grad x - (coarseGrainingDatum a a0 hu hg).v.grad x