Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.Affine.CollarLayerEnvelope

CollarLayerEnvelope #

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

The collar layer envelope of l.piecewise.affine.approx #

|∇ℓ̂_p − p|²  ≤  (648 d)² · 3^{2 b (k + h_k)} · |p|² ,

with the constant explicit and dimension-only. This is exactly the shape of the hF/hG binders of Multiscale.LayerUniform.bounds_on_slopes_when_bad and of …collar_whitneySimplexCells_le_ae, i.e. the collar A antecedent those consumers carry as a hypothesis; Cgrad = 648 d is the value supplied by this local Provider result.

The route #

  1. CompetitorVertexData gives the per-cell estimate |∇ℓ̂_p − p|² ≤ d · (2 |p|_{ℓ¹} D / 3^{scale})², where D bounds the diameter of every component active at the cell's Whitney cube.
  2. The proved local cluster geometry supplies D. Its finiteness — the analytic admissibility of ⨍_{𝒞} — comes from the same node's whitneyNeighborhood_finite_and_mem_leastLayer_or_succ.
  3. The whole scale step is the hypothesis-minimal core (de-privatized) four_mul_three_rpow_layer_envelope_le, which is the only place rpow occurs.
  4. l + h_l ≤ k + h_k turns 3^{b(l+h_l)} into 3^{b(k+h_k)}, and (∑_i |p_i|)² ≤ d |p|² (sq_vecNormOne_le) turns the ℓ¹ size of the slope into its Euclidean square. The constant is 4 · d · d · (4 · 81)² = (648 d)².

The constant, itemized #

Nothing is optimized; the point is that no random quantity, no layer index and no component enters.

No overlap count is consumed #

Under the single-assignment vertex datum of CompetitorVertexData each vertex is claimed by exactly one component, so the per-cell deviation is the max over 𝒜_R, which is bounded by the same layerwise envelope with no cardinality input: the binder hact of …_sub_le_of_forall_touching ranges over exactly 𝒜_R and demands the bound for each of its members. Multiscale.CollarMass.card_le_eleven_pow_of_forall_cubeTouch is therefore not used here; it remains the instrument for the superposition presentation, where the corrections genuinely add.

Scope #

No global function is constructed and no continuity, H¹ membership or subordination is claimed (see the scope section of CompetitorVertexData). The statement is per cell, which is the level at which e.hat.linear.properties states its gradient estimate and the level Multiscale.sum_of_a_decomp (SubadditiveDecomposition.lean) consumes. No layer window is assumed: the layer bookkeeping used here is the proved l.bad.clusters.geometry, whose neighborhood conclusion is proved, not hypothesized.

References #

The scale core #

source
theorem Algsuperdiff.Section3.Provider.Affine.four_mul_three_rpow_layer_envelope_le {b : ℝ} (hb : 0 ≤ b) {a q c : ℕ} (haq : a ≤ q) (hca : c ≤ a + 4) (m : ℤ) :
4 * 3 ^ (b * ↑a) * 3 ^ (m - ↑a) ≤ 324 * 3 ^ (b * ↑q) * 3 ^ (m - ↑c)

The scale step of the layer envelope, isolated from every geometric and measure-theoretic input so that rpow occurs in exactly one place. With a = l + h_l the depth of the diameter bound's anchor layer, q = k + h_k the depth of the cell's own layer and c = (k+1) + h_{k+1} the depth of the cell side, the two hypotheses a ≤ q and c ≤ a + 4 convert the cluster diameter bound into the layer envelope at the cost of 3⁴.

Monotonicity of the closed carrier #

source
theorem Algsuperdiff.Section3.Provider.Affine.closedCubeCarrier_mono {d : ℕ} {J J' : Set (HCPolySupport.TriadicCube d)} (h : J ⊆ J') :
Whitney.closedCubeCarrier J ⊆ Whitney.closedCubeCarrier J'

The active-component diameter datum #

source
theorem Algsuperdiff.Section3.Provider.Affine.active_badComponent_finite_and_diam_le {d : ℕ} {M : ABKModel d} {m : ℤ} {b : ℝ} {hs k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (havoid : ∀ (h : ℕ), hs ≤ h → ∀ u ∈ Percolation.cubeFinset h, ↑(Percolation.badClusterDiam M m h omega u) < 3 ^ (b * ↑h)) {S : Set (HCPolySupport.TriadicCube d)} (hSsub : S ⊆ Whitney.whitneyPartition m (Whitney.whitneyScaleSeq b hs k₀)) (hSbad : ∀ Q ∈ S, omega ∈ BadEvents.bad M Q) {k : ℕ} {R : HCPolySupport.TriadicCube d} (hRlay : R ∈ Whitney.whitneyLayer m (Whitney.whitneyScaleSeq b hs k₀) k) (R' : HCPolySupport.TriadicCube d) :
R' ∈ S → Whitney.CubeTouch R R' → (Whitney.badComponent S R').Finite ∧ Metric.diam (Whitney.closedCubeCarrier (Whitney.badComponent S R')) ≤ 4 * 3 ^ (b * ↑(max (k - 1) 1 + Whitney.whitneyScaleSeq b hs k₀ (max (k - 1) 1))) * 3 ^ (m - ↑(max (k - 1) 1 + Whitney.whitneyScaleSeq b hs k₀ (max (k - 1) 1)))

Every component active at a layer-k Whitney cube is finite and has the layer-k cluster diameter. This is l.bad.clusters.geometry read at the active family 𝒜_□ = {𝒞 : □ ∈ 𝒩(𝒞)}: a bad cube touching □ puts □ in its component's neighborhood, so that neighborhood meets layer k and the proved diameter bound applies to it, hence to the component it contains. Finiteness is the same node's neighborhood finiteness, and is what makes ⨍_{𝒞} ℓ_p an honest average.