SealScalarBase

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

Base infrastructure for the boundary lane's scalar composition

Four ingredients the scalar-control composition consumes, none of them specific to the flush geometry:

• h10FunctionOfSetEq — the H¹₀ transport across a set equality, with exact value and gradient preservation (the H¹₀ sibling of the proved h1FunctionOfSetEq);
• isWeaklyHarmonicOn_sub_h1 — weak Δ-harmonicity is closed under differences;
• eLpNorm_sub_average_translatedCube_le_meanZeroPoincare — the equal-sides mean-zero cube Poincaré at a general translated cube c + □_j ⊆ □_m (the c-and-scale-generic form of BoundaryClauseSkeleton's covering-cube instance, by the same axis-cube realization);
• toReal_eLpNorm_scaleN_cube_le_anchorWindow — the L² transport of a scale-n cube inside the frozen window W' = (z+□_{n+3}) ∩ □_m, at the volume-ratio constant √(27^d).

1. The H¹₀ transport across a set equality

def Algsuperdiff.Section4.Provider.ExcessDecay.h10FunctionOfSetEq {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (h : U = V) (u : HCPolySupport.H10Function U) : HCPolySupport.H10Function V

Transport an H¹₀ function across an equality of its carrier set.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.h10FunctionOfSetEq h u = h ▸ u

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.h10FunctionOfSetEq_toFun {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (h : U = V) (u : HCPolySupport.H10Function U) : (h10FunctionOfSetEq h u).toFun = u.toFun

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.h10FunctionOfSetEq_grad {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (h : U = V) (u : HCPolySupport.H10Function U) : (h10FunctionOfSetEq h u).grad = u.grad

2. Weak harmonicity is closed under differences

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isWeaklyHarmonicOn_sub_h1 {d : ℕ} {V : Set (HCPolySupport.Vec d)} {v₁ v₂ : HCPolySupport.H1Function V} (h₁ : Support.IsWeaklyHarmonicOn V v₁) (h₂ : Support.IsWeaklyHarmonicOn V v₂) : Support.IsWeaklyHarmonicOn V (v₁ - v₂)

Weak Δ-harmonicity is closed under differences.

3. The mean-zero Poincaré at a general translated cube

The general translated-cube Poincaré proof is provided by BoundaryClauseSkeleton.

4. The scale-n window transport

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_anchorWindow_le_scaleN_cube {d : ℕ} (n m : ℤ) (z c' : HCPolySupport.Vec d) : MeasureTheory.volume ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) ≤ ENNReal.ofReal (27 ^ d) * MeasureTheory.volume ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))

The frozen window's volume is at most 27^d times a scale-n cube's.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.toReal_eLpNorm_scaleN_cube_le_anchorWindow {d : ℕ} {n m : ℤ} {z c' : HCPolySupport.Vec d} (hsub : (fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ⊆ (fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) {f : HCPolySupport.Vec d → ℝ} (hfin : MeasureTheory.eLpNorm f 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ≠ ⊤) : (MeasureTheory.eLpNorm f 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))).toReal ≤ √(27 ^ d) * (MeasureTheory.eLpNorm f 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal

The L² transport of a scale-n cube onto the frozen window, at the volume-ratio constant √(27^d).

5. Volume-ratio facts at the frozen window

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_toReal_anchorWindow_le {d : ℕ} (n m : ℤ) (z : HCPolySupport.Vec d) : (MeasureTheory.volume ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))).toReal ≤ (3 ^ (n + 3)) ^ d

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_toReal_anchorWindow_pos {d : ℕ} {n m : ℤ} {z c' : HCPolySupport.Vec d} (hsub : (fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ⊆ (fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : 0 < (MeasureTheory.volume ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))).toReal

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ratio_anchorWindow_coveringCube_le {d : ℕ} (n m : ℤ) (x z : HCPolySupport.Vec d) : (MeasureTheory.volume ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))).toReal / (MeasureTheory.volume ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)))).toReal ≤ 3 ^ d

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ratio_anchorWindow_scaleN_le {d : ℕ} (n m : ℤ) (z c' : HCPolySupport.Vec d) : (MeasureTheory.volume ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))).toReal / (MeasureTheory.volume ((fun (y : HCPolySupport.Vec d) => c' + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))).toReal ≤ 27 ^ d

6. The transfer of a cube mean to the window mean

theorem Algsuperdiff.Section4.Provider.ExcessDecay.abs_avg_cube_sub_window_le {d : ℕ} {m : ℤ} {W A : Set (HCPolySupport.Vec d)} {R : ℝ} (hAm : MeasurableSet A) (hsub : A ⊆ W) (hWm : W ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hWpos : 0 < (MeasureTheory.volume W).toReal) (hApos : 0 < (MeasureTheory.volume A).toReal) (hAtop : MeasureTheory.volume A ≠ ⊤) (hWtop : MeasureTheory.volume W ≠ ⊤) (hR : (MeasureTheory.volume W).toReal / (MeasureTheory.volume A).toReal ≤ R) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) : |HCPolySupport.volumeAverage A u.toFun - HCPolySupport.volumeAverage W u.toFun| ≤ √R * Support.normalizedL2On W fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage W u.toFun