InteriorWindowMove

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

The Gagliardo window move: the child window into the anchor's parent window

InteriorGlueWindow restricts the anchor's clause-(iv) data from □_m to a sub-window — a membership transport, no constant. This module supplies the opposite, quantitative move on the seminorm itself, which the assembly needs on the correction and forcing legs:

  [g]_{H^s(x+□_n)}  ≤  3^{d} · [g]_{H^s(W)} ,      W = (z+□_{n+2}) ∩ □_m ,

whenever the anchor's geometry binder holds. The mechanism is the volume normalization alone: the Gagliardo measure of a window A is |A|^{-1}(vol⊗vol)|_{A×A}, so passing from W to the smaller x+□_n costs exactly the volume ratio |W|/|x+□_n| ≤ 3^{2d} inside an L², i.e. 3^{d}.

The ratio is the two-scale one because the anchor's own geometry binder puts the child x+□_n inside z+□_{n+1}, hence inside z+□_{n+2}, which carries W; the crude bound |W| ≤ |□_{n+2}| = 3^{2d}|□_n| is used, so the constant is 3^{d} and not the 3^{2d} a two-step application would give.

References

• ABK26, l.harmonic.approximation.good.scales, (the geometry binder; the right-hand-side windows).

1. The volume of an origin cube

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_openCubeSet_originCube {d : ℕ} (k : ℤ) : MeasureTheory.volume (HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) = ENNReal.ofReal ((3 ^ k) ^ d)

The open realization of □_k has volume (3^k)^d.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_openCubeSet_originCube_add_two_le {d : ℕ} (n : ℤ) : MeasureTheory.volume (HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) ≤ ENNReal.ofReal (9 ^ d) * MeasureTheory.volume (HCPolySupport.openCubeSet (HCPolySupport.originCube d n))

The two-scale volume ratio of the anchor's parent and child cubes.

2. The seminorm under a window shrink

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedGagliardoESeminormOn_le_of_volume_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {A B : Set (HCPolySupport.Vec d)} {K : ENNReal} (hAB : B ⊆ A) (hK0 : K ≠ 0) (hKtop : K ≠ ⊤) (hvol : MeasureTheory.volume A ≤ K * MeasureTheory.volume B) (s : ℝ) (f : HCPolySupport.Vec d → E) : Support.normalizedGagliardoESeminormOn B s f ≤ K ^ (1 / 2) * Support.normalizedGagliardoESeminormOn A s f

The Gagliardo seminorm on a sub-window, at the volume ratio.

If B ⊆ A and |A| ≤ K |B| then [f]_{H^s(B)} ≤ K^{1/2} [f]_{H^s(A)}. Both sides are ℝ≥0∞, so no finiteness is required.

3. The anchor's child-to-parent window move

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

The d-only constant of the window move: 3^d, the square root of the two-scale volume ratio.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.gagliardoWindowConst d = 3 ^ d

theorem Algsuperdiff.Section4.Provider.ExcessDecay.gagliardoWindowConst_pos (d : ℕ) : 0 < gagliardoWindowConst d

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedGagliardoESeminormOn_child_le_anchorWindow {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n m : ℤ} {x z : HCPolySupport.Vec d} (hgeom : (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 1)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (s : ℝ) (f : HCPolySupport.Vec d → E) : Support.normalizedGagliardoESeminormOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) s f ≤ ENNReal.ofReal (gagliardoWindowConst d) * Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s f

The window move.

Under the anchor's geometry binder, the Gagliardo seminorm on the child window x + □_n is bounded by 3^d times the seminorm on the anchor's own right-hand-side window W = (z+□_{n+2}) ∩ □_m.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedGagliardoESeminormOn_child_toReal_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n m : ℤ} {x z : HCPolySupport.Vec d} {s : ℝ} (hgeom : (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 1)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (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 + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) : (Support.normalizedGagliardoESeminormOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) s f).toReal ≤ gagliardoWindowConst d * (Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s f).toReal

The window move, in the real-valued form the assembly consumes.

The finiteness hypothesis is the anchor's own clause (iv), restricted to W.