TranslationTransport

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

The A4 translation transport of the weak equation

The frozen theorem's own datum lives at the untranslated sample ω on the window z + □_{n+2}. This module moves the weak equation between the two frames.

Two ingredients, both exact:

• the function side — H1Function.untranslate z / H10Function.translate, with the Lebesgue change of variables setIntegral_comp_addRight_translateSet. The translated frame's solution is x ↦ u(x + z) and its forcing x ↦ g(x + z).
• the coefficient side — Cutoff.coefficientCutoff_translateCutoffSample: a_L(·, translateCutoffSample z ω) = a_L(· + z, ω) exactly, as regular coefficient fields. So the translated frame's coefficient field is the cutoff coefficient of the translated sample; nothing is lost or approximated.

Main results

• isDivFormWeakSolutionOn_untranslate — the weak equation on translateSet z U becomes the weak equation on U for the back-translated data.
• isOpen_translateSet_openCubeSet, translateSet_openCubeSet_subset_of_frontier_inter_empty — the anchor's window and its interior gate in translateSet spelling.
• coefficientCutoff_comp_add_eq_translateCutoffSample — the coefficient side.
• isDivFormWeakSolutionOn_translateCutoffSample — the two combined: from the anchor's frame to the harmonic slot's frame in one step.

References

• ABK26, l.harmonic.approximation.good.scales, (the frame of the good event 𝒢(n+2, z; s/8, 1/2) and of 𝓔(z+□_{n+2})).
• The translated-sample convention: a cube translate is realized by translating the sample, never the cube.
• CoarseGraining, Homogenization/Sobolev/H1/Translation.lean, Homogenization/Geometry/Translation.lean (setIntegral_comp_addRight_translateSet).
• Repo, Algsuperdiff/Section3/Cutoff/Symmetry.lean (coefficientCutoff_translateCutoffSample).

1. The weak equation untranslates

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isDivFormWeakSolutionOn_untranslate {d : ℕ} {U : Set (HCPolySupport.Vec d)} (z : HCPolySupport.Vec d) {a : HCPolySupport.CoeffField d} {u : HCPolySupport.H1Function (HCPolySupport.translateSet z U)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (h : Support.IsDivFormWeakSolutionOn a (HCPolySupport.translateSet z U) u g) : Support.IsDivFormWeakSolutionOn (fun (x : HCPolySupport.Vec d) => a (x + z)) U (HCPolySupport.H1Function.untranslate z u) fun (x : HCPolySupport.Vec d) => g (x + z)

The divergence-form weak equation in the back-translated frame.

If -∇·a∇u = ∇·g weakly on U + z, then -∇·ã∇u_tilde = ∇·g weakly on U, where every datum is precomposed with x ↦ x + z. Exact: the change of variables is measure preserving and the H¹₀ test functions correspond bijectively.

2. The window in translateSet spelling

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isOpen_translateSet_openCubeSet {d : ℕ} (z : HCPolySupport.Vec d) (k : ℤ) : IsOpen (HCPolySupport.translateSet z (HCPolySupport.openCubeSet (HCPolySupport.originCube d k)))

The frozen theorem's translated window, written as CoarseGraining's translateSet, is open.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.translateSet_openCubeSet_subset_of_frontier_inter_empty {d : ℕ} {k m : ℤ} {z : HCPolySupport.Vec d} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hfr : (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k) ∩ frontier (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) = ∅) : HCPolySupport.translateSet z (HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

3. The coefficient side

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

The cutoff coefficient of the translated sample is the translated cutoff coefficient, as raw coefficient fields. This is what makes the translated frame's coefficient field the manuscript's own a_L at translateCutoffSample z ω rather than an approximation.

4. The two frames, combined

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isDivFormWeakSolutionOn_translateCutoffSample {d : ℕ} {S : Set (HCPolySupport.Vec d)} (M : Section3.ABKModel d) (L : ℤ) (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) {u : HCPolySupport.H1Function (HCPolySupport.translateSet z S)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (h : Support.IsDivFormWeakSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.translateSet z S) u g) : Support.IsDivFormWeakSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L (Section3.Cutoff.translateCutoffSample z omega)).toCoeffField S (HCPolySupport.H1Function.untranslate z u) fun (x : HCPolySupport.Vec d) => g (x + z)

From the anchor's frame to the harmonic slot's frame.

The anchor's equation -∇·a_L(·,ω)∇u = ∇·g on the window z + S becomes, on S itself, the equation for the cutoff coefficient at the translated sample translateCutoffSample z ω, with solution u(· + z) and forcing g(· + z). This is the A4 transport of the equation leg.