ResidueFlushTransport

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

The one-step window transport K' → W'

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

What is proved

The proved boundary composition transports the child cube's Gagliardo seminorm to the frozen window W' = (z+□_{n+3}) ∩ □_m in two hops, the anchor's child window x + □_n ⊆ (z+□_{n+2}) ∩ □_m and then the window move onto W', at the constants gagliardoWindowConst d = 3^d and windowMoveConst d = 9^d. The flush sub-cube K' = flushSubCentre z m n i σ + □_n is not inside (z+□_{n+2}) ∩ □_m (that is ResidueAbsorption's block), so the two-hop route is unavailable.

It is not needed: K' ⊆ W' is proved (SealCaccioppoliGeometry.flushSubCube_subset_anchorWindow) and the volume ratio |W'| ≤ 27^d |K'| is proved (SealScalarBase.volume_anchorWindow_le_scaleN_cube), so InteriorWindowMove.normalizedGagliardo gives the one-hop transport at √(27^d) — the same constant ResidueInterface already uses for the L² transport at K'. Note √(27^d) ≤ 3^d·9^d = 27^d, so the one-hop constant is no worse than the proved two-hop product.

References

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

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.flushWindowConst (d : ℕ) : ℝ

The one-hop window constant √(27^d), the same factor ResidueInterface uses for the L² transport at the flush sub-cube.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.flushWindowConst d = √(27 ^ d)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.flushWindowConst_pos (d : ℕ) : 0 < flushWindowConst d

theorem Algsuperdiff.Section4.Provider.ExcessDecay.flushWindowConst_nonneg (d : ℕ) : 0 ≤ flushWindowConst d

1. The Gagliardo seminorm, transported in one hop

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedGagliardoESeminormOn_flushSubCube_le_anchorWindow {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n m : ℤ} (hnm : n + 2 ≤ m) {z : HCPolySupport.Vec d} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (i : Fin d) {σ : ℝ} (hσ : σ = 1 ∨ σ = -1) (s : ℝ) (f : HCPolySupport.Vec d → E) : Support.normalizedGagliardoESeminormOn ((fun (y : HCPolySupport.Vec d) => flushSubCentre z m n i σ + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) s f ≤ ENNReal.ofReal (flushWindowConst d) * Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s f

The one-hop Gagliardo transport at the flush sub-cube.

[f]_{H^s(K')} ≤ √(27^d) · [f]_{H^s(W')}, from K' ⊆ W' and |W'| ≤ 27^d |K'|. Both sides are ℝ≥0∞, so no finiteness hypothesis is needed.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedGagliardoESeminormOn_flushSubCube_toReal_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n m : ℤ} (hnm : n + 2 ≤ m) {z : HCPolySupport.Vec d} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (i : Fin d) {σ s : ℝ} (hσ : σ = 1 ∨ σ = -1) (f : HCPolySupport.Vec d → E) (hfin : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 f) 2 (Support.normalizedGagliardoMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) : (Support.normalizedGagliardoESeminormOn ((fun (y : HCPolySupport.Vec d) => flushSubCentre z m n i σ + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) s f).toReal ≤ flushWindowConst d * (Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s f).toReal

The one-hop Gagliardo transport, in the real-valued spelling the composition consumes.

2. The window's volume is nonzero, from the flush sub-cube

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_anchorWindow_ne_zero_of_flushSubCube {d : ℕ} {n m : ℤ} (hnm : n + 2 ≤ m) {z : HCPolySupport.Vec d} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (i : Fin d) {σ : ℝ} (hσ : σ = 1 ∨ σ = -1) : MeasureTheory.volume ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) ≠ 0

W' carries positive volume, because the flush sub-cube does and sits inside it. The proved derivation goes through the (n+2) window and the anchor's geometry binder; at K' this is the direct route.