SealMeanCube

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

(A) at a cube: the flush-face mean bound with a dimension-only constant

MeanFinalMeanBound.exists_abs_le_normalizedL2On_of_faceOdd proves the mean bound (A) for an abstract near-face geometry: four sets S ⊆ K ⊆ D, S ⊆ T ⊆ D, a signed depth w, a ball radius r, and two volume ratios, subject to a list of inclusions and an absorption room hypothesis. This module instantiates that statement at the geometry the composition actually has — a cube with a flush face — and discharges every geometric side condition, leaving a clean statement

  |β| ≤ C(d) · ‖W − β‖_{L²(K)} ,     K = sealCube c L ,

for W odd about the face hyperplane {yᵢ = c i + σ·L/2} (σ = ±1) and W − β classically harmonic on the doubled cube sealDouble c L i σ. The constant depends on the dimension only: neither the centre c, nor the side L > 0, nor the coordinate i, nor the sign σ occurs in it.

The choice of parameters

With the dimensional constant of exists_abs_le_normalizedL2On_of_faceOdd,

  r = L/8 ,   λ = (16 + 1152·CH·4ᵈ)⁻¹ ,   w = σ·(λL) ,   RK = √(λ⁻¹ᵈ) ,  RD = 4ᵈ ,
  C(d) = 6·√(λ⁻¹ᵈ) + 12·(64·CH·4ᵈ·λ²)   ( ≤ 6·√(λ⁻¹ᵈ) + 1 ) .

The two ratios are the crude volume bounds |K| ≤ Lᵈ, |S| ≥ (λL)ᵈ, |D| ≤ (2L)ᵈ, rᵈ = (L/8)ᵈ. The room hypothesis is CH·r⁻¹·r⁻¹·RD·w² = 64·CH·4ᵈ·λ² with 9·(64·CH·4ᵈ·λ²) ≤ 1/2, i.e. 1152·CH·4ᵈ·λ² ≤ 1, which holds because 1152·CH·4ᵈ ≤ (16 + 1152·CH·4ᵈ)² = λ⁻² for every CH·4ᵈ ≥ 0 (the degenerate value CH·4ᵈ = 0 makes the left side vanish). All six windows are open coordinate boxes that are cubes transversally to i with a prescribed i-edge; they are packaged as axisBox, whose small A (inclusion, reflection, translation, sup-ball, two volume bounds) is what makes the two sign branches short.

Naming: the relation to SealCaccioppoliGeometry

That module fixes the parent scale at n + 2 and exports flushSubCentre z m n i σ in Algsuperdiff.Section4.Provider.ExcessDecay. Everything named flushSub… here carries the seal prefix (sealFlushSubCentre z m k n i sg, with the parent scale k a free index) so that a consumer may open both namespaces; the bodies are written in the same if-normal form, so sealFlushSubCentre z m (n+2) n i σ = flushSubCentre z m n i σ holds by rfl. The bridge is not stated here: this module does not import that one.

What is not done here

Nothing analytic: no Taylor step, no Hessian estimate, no harmonicity is proved. The single analytic input is the abstract (A) of MeanFinalMeanBound; the square integrability of W on the doubled cube and the classical harmonicity of W − β there remain hypotheses of every statement below.

References

• ABK26, l.harmonic.approximation.good.scales, Step 2 (boundary cubes).

1. Axis boxes

An axisBox is the open box which is a cube of half-side b about c in every coordinate except i, and has the prescribed edge (p, q) in the coordinate i. All six windows of the instantiation are of this shape.

def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.axisLo {d : ℕ} (c : HCPolySupport.Vec d) (i : Fin d) (p b : ℝ) : Fin d → ℝ

The lower corner of the box with i-edge (p, q) and transversal half-side b.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.axisLo c i p b j = if j = i then p else c j - b

def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.axisHi {d : ℕ} (c : HCPolySupport.Vec d) (i : Fin d) (q b : ℝ) : Fin d → ℝ

The upper corner of the box with i-edge (p, q) and transversal half-side b.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.axisHi c i q b j = if j = i then q else c j + b

def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.axisBox {d : ℕ} (c : HCPolySupport.Vec d) (i : Fin d) (p q b : ℝ) : Set (HCPolySupport.Vec d)

The open box with i-edge (p, q) and transversal half-side b about c.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.axisLo_self {d : ℕ} {c : HCPolySupport.Vec d} {i : Fin d} {p b : ℝ} : axisLo c i p b i = p

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.axisLo_of_ne {d : ℕ} {c : HCPolySupport.Vec d} {i j : Fin d} {p b : ℝ} (hji : j ≠ i) : axisLo c i p b j = c j - b

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.axisHi_self {d : ℕ} {c : HCPolySupport.Vec d} {i : Fin d} {q b : ℝ} : axisHi c i q b i = q

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.axisHi_of_ne {d : ℕ} {c : HCPolySupport.Vec d} {i j : Fin d} {q b : ℝ} (hji : j ≠ i) : axisHi c i q b j = c j + b

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.mem_axisBox_iff {d : ℕ} {c : HCPolySupport.Vec d} {i : Fin d} {p q b : ℝ} {y : HCPolySupport.Vec d} : y ∈ axisBox c i p q b ↔ (p < y i ∧ y i < q) ∧ ∀ (j : Fin d), j ≠ i → c j - b < y j ∧ y j < c j + b

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.convex_axisBox {d : ℕ} (c : HCPolySupport.Vec d) (i : Fin d) (p q b : ℝ) : Convex ℝ (axisBox c i p q b)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.measurableSet_axisBox {d : ℕ} (c : HCPolySupport.Vec d) (i : Fin d) (p q b : ℝ) : MeasurableSet (axisBox c i p q b)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.volume_axisBox_ne_top {d : ℕ} (c : HCPolySupport.Vec d) (i : Fin d) (p q b : ℝ) : MeasureTheory.volume (axisBox c i p q b) ≠ ⊤

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.axisBox_subset_axisBox {d : ℕ} {c : HCPolySupport.Vec d} {i : Fin d} {p q b p' q' b' : ℝ} (hp : p' ≤ p) (hq : q ≤ q') (hb : b ≤ b') : axisBox c i p q b ⊆ axisBox c i p' q' b'

Widening the i-edge and the transversal half-side enlarges the box.

Translating in the i direction

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sub_smul_basisVec_apply_self {d : ℕ} (y : HCPolySupport.Vec d) (w : ℝ) (i : Fin d) : (y - w • HCPolySupport.basisVec i) i = y i - w

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sub_smul_basisVec_apply_of_ne {d : ℕ} (y : HCPolySupport.Vec d) (w : ℝ) {i j : Fin d} (hji : j ≠ i) : (y - w • HCPolySupport.basisVec i) j = y j

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sub_smul_basisVec_mem_axisBox {d : ℕ} {c : HCPolySupport.Vec d} {i : Fin d} {p q b p' q' b' w : ℝ} {y : HCPolySupport.Vec d} (hy : y ∈ axisBox c i p q b) (hp : p' ≤ p - w) (hq : q - w ≤ q') (hb : b ≤ b') : y - w • HCPolySupport.basisVec i ∈ axisBox c i p' q' b'

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.image_sub_smul_axisBox_subset {d : ℕ} {c : HCPolySupport.Vec d} {i : Fin d} {p q b p' q' b' w : ℝ} (hp : p' ≤ p - w) (hq : q - w ≤ q') (hb : b ≤ b') : (fun (z : HCPolySupport.Vec d) => z - w • HCPolySupport.basisVec i) '' axisBox c i p q b ⊆ axisBox c i p' q' b'

Reflecting about a hyperplane transversal to i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.coordFaceReflection_mem_axisBox {d : ℕ} {c : HCPolySupport.Vec d} {i : Fin d} {p q b p' q' b' a : ℝ} {y : HCPolySupport.Vec d} (hy : y ∈ axisBox c i p q b) (hp : p' ≤ 2 * a - q) (hq : 2 * a - p ≤ q') (hb : b ≤ b') : HCPolySupport.coordFaceReflection a i y ∈ axisBox c i p' q' b'

The sup-ball family

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.metricBall_subset_axisBox {d : ℕ} {c : HCPolySupport.Vec d} {i : Fin d} {p q b p' q' b' r : ℝ} (hr : 0 < r) {z : HCPolySupport.Vec d} (hz : z ∈ axisBox c i p q b) (hp : p' ≤ p - r) (hq : q + r ≤ q') (hb : b + r ≤ b') : Metric.ball z r ⊆ axisBox c i p' q' b'

Two crude volume bounds

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.pow_le_volume_toReal_axisBox {d : ℕ} {c : HCPolySupport.Vec d} {i : Fin d} {p q b e : ℝ} (he : 0 ≤ e) (hmet : e ≤ q - p) (hb : e ≤ 2 * b) : e ^ d ≤ (MeasureTheory.volume (axisBox c i p q b)).toReal

Lower-bounding every edge of an axis box by the same number.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.volume_toReal_axisBox_le_pow {d : ℕ} {c : HCPolySupport.Vec d} {i : Fin d} {p q b e : ℝ} (hpq : p ≤ q) (hb0 : 0 ≤ b) (hmet : q - p ≤ e) (hb : 2 * b ≤ e) : (MeasureTheory.volume (axisBox c i p q b)).toReal ≤ e ^ d

Upper-bounding every edge of an axis box by the same number.

2. The cube and the cube doubled across a face

def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sealCube {d : ℕ} (c : HCPolySupport.Vec d) (L : ℝ) : Set (HCPolySupport.Vec d)

The cube of centre c and side L.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sealCube c L = Algsuperdiff.Section4.Provider.ExcessDecay.coordBox (fun (j : Fin d) => c j - L / 2) fun (j : Fin d) => c j + L / 2

def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sealDouble {d : ℕ} (c : HCPolySupport.Vec d) (L : ℝ) (i : Fin d) (sg : ℝ) : Set (HCPolySupport.Vec d)

The cube of centre c and side L, doubled across its σeᵢ face (σ = ±1).

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.mem_sealCube_iff {d : ℕ} {c : HCPolySupport.Vec d} {L : ℝ} {y : HCPolySupport.Vec d} : y ∈ sealCube c L ↔ ∀ (j : Fin d), c j - L / 2 < y j ∧ y j < c j + L / 2

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sealCube_eq_axisBox {d : ℕ} (c : HCPolySupport.Vec d) (L : ℝ) (i : Fin d) : sealCube c L = axisBox c i (c i - L / 2) (c i + L / 2) (L / 2)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sealDouble_eq_axisBox {d : ℕ} (c : HCPolySupport.Vec d) (L : ℝ) (i : Fin d) {sg : ℝ} (hsg : sg = 1 ∨ sg = -1) : sealDouble c L i sg = axisBox c i (c i + sg * (L / 2) - L) (c i + sg * (L / 2) + L) (L / 2)

3. The two volume ratios and the absorption coefficient

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sqrt_volume_slab_ratio_le {d : ℕ} {vK vS L lam : ℝ} (hL : 0 < L) (hlam : 0 < lam) (hK : vK ≤ L ^ d) (hS : (lam * L) ^ d ≤ vS) : √(vK / vS) ≤ √(lam⁻¹ ^ d)

The slab ratio √(|K|/|S|) is bounded by the dimension-only √(λ⁻¹ᵈ).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sqrt_volume_ball_ratio_le {d : ℕ} {vD L : ℝ} (hL : 0 < L) (hD : vD ≤ (2 * L) ^ d) : √(vD / (L / 8) ^ d) ≤ 4 ^ d

The Hessian ratio √(|D|/rᵈ) is bounded by the dimension-only 4ᵈ.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.coef_eq_of_sq {d : ℕ} {CH L lam w : ℝ} (hL0 : L ≠ 0) (hw : w ^ 2 = (lam * L) ^ 2) : CH * (L / 8)⁻¹ * (L / 8)⁻¹ * 4 ^ d * w ^ 2 = 64 * (CH * 4 ^ d) * lam ^ 2

The absorption coefficient at r = L/8, with the ratio bound 4ᵈ and w² = (λL)².

4. (A) at a cube with a flush face

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.exists_abs_le_normalizedL2On_sealCube (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (i : Fin d) (sg L : ℝ) (c : HCPolySupport.Vec d) (W : HCPolySupport.Vec d → ℝ) (beta : ℝ), sg = 1 ∨ sg = -1 → 0 < L → (∀ (z : HCPolySupport.Vec d), W (HCPolySupport.coordFaceReflection (c i + sg * (L / 2)) i z) = -W z) → MeasureTheory.MemLp W 2 (MeasureTheory.volume.restrict (sealDouble c L i sg)) → InnerProductSpace.HarmonicOnNhd ((fun (y : HCPolySupport.Vec d) => W y - beta) ∘ ⇑toEuc.symm) (⇑toEuc '' sealDouble c L i sg) → |beta| ≤ C * Support.normalizedL2On (sealCube c L) fun (y : HCPolySupport.Vec d) => W y - beta

5. The flush cube of the well-placed clamp

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.image_add_eq_sealCube {d : ℕ} (c : HCPolySupport.Vec d) (j : ℤ) : (fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d j) = sealCube c (3 ^ j)

A translated open triadic cube is a sealCube.

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sealFlushSubCentre {d : ℕ} (z : HCPolySupport.Vec d) (m k n : ℤ) (i : Fin d) (sg : ℝ) : HCPolySupport.Vec d

The centre of the flush sub-cube of side 3ⁿ sharing the σeᵢ face of the well-placed cube of side 3ᵏ.

The body is written in the if-normal form of SealCaccioppoliGeometry.flushSubCentre, so that at k = n + 2 the two definitions are the same term; see the module docstring.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sealFlushSubCentre_apply {d : ℕ} (z : HCPolySupport.Vec d) (m k n : ℤ) (i : Fin d) (sg : ℝ) (r : Fin d) : sealFlushSubCentre z m k n i sg r = wellPlacedCentre z m k r + if r = i then sg * ((3 ^ k - 3 ^ n) / 2) else 0

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sealFlushSubCentre_apply_self {d : ℕ} (z : HCPolySupport.Vec d) (m k n : ℤ) (i : Fin d) (sg : ℝ) : sealFlushSubCentre z m k n i sg i = wellPlacedCentre z m k i + sg * ((3 ^ k - 3 ^ n) / 2)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sealFlushSubCentre_faceLevel {d : ℕ} {m k n : ℤ} (hkm : k ≤ m) {z : HCPolySupport.Vec d} {i : Fin d} {sg : ℝ} (hsg : sg = 1 ∨ sg = -1) (hover : wellPlacedHalfGap m k < sg * z i) : sealFlushSubCentre z m k n i sg i + sg * (3 ^ n / 2) = sg * (1 / 2 * 3 ^ m)

The flush face sits in the frontier hyperplane.

On the boundary branch the σeᵢ face of the well-placed cube of side 3ᵏ lies exactly in {σ yᵢ = ½·3ᵐ}, and so does the σeᵢ face of the concentric-in-σeᵢ sub-cube of side 3ⁿ centred at sealFlushSubCentre z m k n i σ.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.exists_abs_le_normalizedL2On_sealFlushSubCube (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (m k n : ℤ) (z : HCPolySupport.Vec d) (i : Fin d) (sg : ℝ) (W : HCPolySupport.Vec d → ℝ) (beta : ℝ), k ≤ m → sg = 1 ∨ sg = -1 → wellPlacedHalfGap m k < sg * z i → (∀ (y : HCPolySupport.Vec d), W (HCPolySupport.coordFaceReflection (sg * (1 / 2 * 3 ^ m)) i y) = -W y) → MeasureTheory.MemLp W 2 (MeasureTheory.volume.restrict (sealDouble (sealFlushSubCentre z m k n i sg) (3 ^ n) i sg)) → InnerProductSpace.HarmonicOnNhd ((fun (y : HCPolySupport.Vec d) => W y - beta) ∘ ⇑toEuc.symm) (⇑toEuc '' sealDouble (sealFlushSubCentre z m k n i sg) (3 ^ n) i sg) → |beta| ≤ C * Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => sealFlushSubCentre z m k n i sg + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (y : HCPolySupport.Vec d) => W y - beta

(A) at the flush sub-cube of the boundary branch.

At the boundary branch of the covering — the overhang wellPlacedHalfGap m k < σ·zᵢ — the cube of side 3ⁿ centred at sealFlushSubCentre z m k n i σ has its σeᵢ face exactly in the frontier hyperplane {σ yᵢ = ½·3ᵐ}, so the flush-cube mean bound applies there verbatim, with the same dimension-only constant. The scale-k well-placed cube itself is the case n = k.