BoundaryDatumTransport

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

The A4 sample transport of the boundary Caccioppoli datum

This module performs the A4 move — translation in the sample — for all three ingredients of the datum, so that the whole boundary display can be read at originCube d k and at Cutoff.translateCutoffSample c ω:

  equation        -∇·a_L(·,ω)∇u = ∇·g   on c + □_k
                    ↦  -∇·ã_{L,k}(·, τ_c ω)∇u(·+c) = ∇·(-g(·+c))   on □_k
  boundary datum  LocalizedZeroTrace (c+□_k) (patch at x)  ρ
                    ↦  LocalizedZeroTrace □_k (patch at x-c)  ρ(·+c)
  covering        ⨍_{(x+□_{k-2})∩□_m} f  ≤  3^d ⨍_{core □_k (x-c)} f(·+c)

Nothing analytic happens here: every step is an exact change of variables.

The frame, spelled out (disclosed)

The Caccioppoli patch centre moves with the frame: in the translated frame the anchor's window (x+□_j)∩□_m is centred at x, in □_k's own frame it is centred at x - c.

References

• ABK26, l.coarse.grained.Caccioppoli.RHS; the covering argument.
• CoarseGraining, Sobolev/H1/Translation.lean, Sobolev/H1/LocalizedZeroTrace.lean.

1. The covering cube in translateSet spelling

theorem Algsuperdiff.Section4.Provider.ExcessDecay.translateSet_wellPlacedCentre_subset {d : ℕ} {m k : ℤ} (x : HCPolySupport.Vec d) (hkm : k ≤ m) : HCPolySupport.translateSet (wellPlacedCentre x m k) (HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

The well-placed covering cube fits inside the domain, written with CoarseGraining's translateSet — the spelling the translation transport is stated at.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.openCubeAtScale_eq_translateSet {d : ℕ} (c w : HCPolySupport.Vec d) (j : ℤ) : HCPolySupport.Book.Ch03.openCubeAtScale w j = HCPolySupport.translateSet c (HCPolySupport.Book.Ch03.openCubeAtScale (w - c) j)

The Dirichlet patch moves with the frame: x + □_j seen from c is (x - c) + □_j.

2. The boundary datum transports

theorem Algsuperdiff.Section4.Provider.ExcessDecay.localizedZeroTraceFunctionOn_untranslate {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (c : HCPolySupport.Vec d) {f : HCPolySupport.Vec d → ℝ} (h : HCPolySupport.LocalizedZeroTraceFunctionOn (HCPolySupport.translateSet c U) (HCPolySupport.translateSet c V) f) : HCPolySupport.LocalizedZeroTraceFunctionOn U V fun (y : HCPolySupport.Vec d) => f (y + c)

The localized zero trace untranslates.

If f has the localized zero trace on U + c through the window V + c, then f(· + c) has it on U through V. The cutoffs correspond bijectively under η ↦ η(· - c), and CoarseGraining's H10Function.untranslate carries the witness.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.localizedZeroTraceFunctionOn_wellPlacedCube_untranslate {d : ℕ} {m k : ℤ} (x : HCPolySupport.Vec d) (hkm : k ≤ m) (rho : HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) : HCPolySupport.LocalizedZeroTraceFunctionOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) (HCPolySupport.Book.Ch03.openCubeAtScale (x - wellPlacedCentre x m k) (k - 1)) fun (y : HCPolySupport.Vec d) => rho.toFun (y + wellPlacedCentre x m k)

The anchor's Dirichlet datum, on the covering cube, in its own frame.

The H¹₀(□_m) witness ρ = u - h of the frozen theorem's boundary condition gives the localized zero trace that CoarseGraining's BoundaryForcedCaccioppoliDatum asks for at the outer cube □_k and patch centre x - c.

3. The equation transports

4. The covering inequality, in the covering cube's own frame

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedSetAverage_truncatedWindow_le_three_pow_mul_untranslatedCore {d : ℕ} {m k : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k ≤ m) {f : HCPolySupport.Vec d → ℝ} (hf : ∀ y ∈ (fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m k + y) '' HCPolySupport.Book.Ch03.caccioppoliCoreSet (HCPolySupport.originCube d k) (x - wellPlacedCentre x m k), 0 ≤ f y) (hint : MeasureTheory.IntegrableOn f ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m k + y) '' HCPolySupport.Book.Ch03.caccioppoliCoreSet (HCPolySupport.originCube d k) (x - wellPlacedCentre x m k)) MeasureTheory.volume) : HCPolySupport.Book.Ch03.normalizedSetAverage (truncatedWindow x m (k - 2)) f ≤ 3 ^ d * HCPolySupport.Book.Ch03.normalizedSetAverage (HCPolySupport.Book.Ch03.caccioppoliCoreSet (HCPolySupport.originCube d k) (x - wellPlacedCentre x m k)) fun (y : HCPolySupport.Vec d) => f (y + wellPlacedCentre x m k)

The covering step, transported.

The normalized average of a nonnegative integrand over the frozen theorem's own window (x+□_{k-2}) ∩ □_m is at most 3^d times its normalized average over CoarseGraining's Caccioppoli core caccioppoliCoreSet (□_k) (x - c) in the covering cube's own frame, the integrand being read at the translated point.

5. The energy density is frame-inert

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedSetAverage_const_mul {d : ℕ} (V : Set (HCPolySupport.Vec d)) (c : ℝ) (f : HCPolySupport.Vec d → ℝ) : (HCPolySupport.Book.Ch03.normalizedSetAverage V fun (y : HCPolySupport.Vec d) => c * f y) = c * HCPolySupport.Book.Ch03.normalizedSetAverage V f

The normalized average is homogeneous in a scalar factor.