BadSetDefinitions #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
d.whitney.bad-set.definitions: the Whitney partition and its bad set #
This module defines local implementations of the definitions in ABK26's
sss.whitney.partition:
- the scale separation sequence
h_n = ⌈b(1-b)⁻¹ n⌉ + h_hat_sep + k₀(e.hn.def) and the one-layer gaph_{n+1} - h_n ≤ 1(e.hn.gap, (label-line convention;)); - the recursive Whitney partition
𝒲(□_m)and its layers𝒲(□_m, n)(e.W.n.def); - the bad family
ℐandℐ_n(e.bad.cubes.in.partition); - the neighborhood
𝒩(𝒥)(e.neighborhood.def); - connected components of
ℐ.
The recursion, unrolled #
The manuscript's construction is: divide □_m into its 3^d children; a child
that touches ∂□_m is carried to the next layer and re-divided; a child that
does not touch ∂□_m is a layer-n cube and is subdivided h_n further
generations. The cubes so produced are the elements of 𝒲(□_m).
A cube reaches layer n exactly when every one of its ancestors of depth
1, …, n-1 touches ∂□_m, and by touchesBoundary_of_mem_descendantsAtDepth
that is the same as its depth-(n-1) ancestor touching ∂□_m. So the layer is
the closed-form family
𝒲(□_m, n) = ⋃ { descendantsAtDepth C (h n) :
C a non-touching child of a touching depth-(n-1) descendant } ,
which is the definition taken here (whitneyLayer). 𝒲(□_m) is the union of
all layers, without any fuel truncation. whitneyLayer_eq_filter_scale proves
that this agrees with the manuscript's own e.W.n.def, which defines
𝒲(□_m, n) as the cubes of 𝒲(□_m) of size 3^{m-n-h_n}.
Carriers #
Cubes are Homogenization.TriadicCube d; □_m is originCube d m; triadic
subdivision is childCubes / descendantsAtDepth. "□ touches ∂□_m" is
the extreme-index predicate TouchesBoundary: a depth-t descendant of □_m
is the box (index ± ½)·3^{m-t}, and □_m is (0 ± ½)·3^m, so the closed
cube meets ∂□_m in the coordinate i exactly when index i = ±(3^t - 1)/2 = ±E_t. The bad event 𝓑(□) is the proved BadEvents.bad.
Reading notes (recorded) #
𝒩(𝒥)is defined through∃ □' ∈ 𝒥, dist(□,□') = 0rather than throughdist(□, ⋃𝒥) = 0. The two agree whenever𝒥is finite, and every manuscript use of𝒩is at a bad cluster; the pointwise form is the one the proofs consume.dist(□,□') = 0for the closed cubes isCubeTouch, characterized coordinatewise bycubeTouch_iff.
References #
- ABK26,
sss.whitney.partition.
The scale separation sequence e.hn.def #
ABK26 e.hn.def: the scale separation sequence h_n = ⌈b (1-b)⁻¹ n⌉ + h_hat_sep + k₀, as a function of the value hs of the minimal scale separation
h_hat_sep and of the parameter k₀.
Equations
Instances For
h_n ≥ h_hat_sep + k₀: the bottom of the sequence, used to check the
h ≥ h_hat_sep hypothesis of the deterministic percolation bounds.
ABK26 e.hn.gap: for b ≤ 1/8 consecutive scale separations differ by at
most one, so the Whitney scales grow by at most one layer at a time.
The Whitney depth sequence anchored at the sample's separation height.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Boundary-index arithmetic #
E_j = (3^j - 1)/2, the extreme index coordinate of a depth-j triadic
descendant of □_m.
Equations
Instances For
□ touches ∂□_m: some index coordinate of □ is extreme. For a
depth-t descendant of □_m, whose closed realization is the box
(index ± ½)·3^{m-t} inside □_m = (0 ± ½)·3^m, this is exactly the condition
that the closed cube meets the boundary ∂□_m.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Triadic subdivision #
The index of a depth-s descendant stays within E_s of the rescaled index
of its ancestor.
Boundary touching propagates from a child to its parent.
Boundary touching propagates to ancestors. Contrapositive: no descendant
of a cube in the interior of □_m ever touches ∂□_m.
The Whitney partition #
ABK26 𝒲(□_m, n): the layer-n cubes of the Whitney partition of □_m at
the scale profile hn. A layer-n cube is a depth-h_n triadic descendant
of a child C of a boundary-touching depth-(n-1) descendant A of □_m,
where C itself does not touch ∂□_m. Layer 0 is empty: the recursion
starts at layer 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
ABK26 𝒲(□_m): the Whitney partition, the union of all its layers. No
truncation: the family is the literal infinite one.
Equations
Instances For
e.W.n.def, the size clause: every layer-n cube has size 3^{m-n-h_n}.
A layer-n cube is a depth-(n + h_n) triadic descendant of □_m.
The termination clause: no element of 𝒲(□_m) touches ∂□_m.
Distinct layers are disjoint.
The bad cubes of the partition #
ABK26 e.bad.cubes.in.partition: the bad family ℐ = {□ ∈ 𝒲(□_m): 𝓑(□) occurs}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
ABK26 ℐ_n = ℐ ∩ 𝒲(□_m, n): the bad cubes of layer n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Adjacency, neighborhoods and components #
dist(□, □') = 0 in the manuscript's ℓ^∞ sense: the closed cubes
intersect. On Vec d = Fin d → ℝ the ambient metric is the sup metric and
Metric.closedBall (cubeCenter Q) (cubeRadius Q) is the closed realization of
the triadic cube Q.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The coordinatewise characterization of touching.
ABK26 e.neighborhood.def: the neighborhood 𝒩(𝒥) = {□ ∈ 𝒲(□_m): dist(□, 𝒥) = 0} of a subfamily 𝒥 ⊆ 𝒲(□_m), read cubewise (see the module docstring).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The chain relation: Q and R are joined by a chain of pairwise adjacent
cubes of J.
Equations
- Algsuperdiff.Section3.Provider.Whitney.BadChain J = Relation.ReflTransGen fun (A B : HCPolySupport.TriadicCube d) => A ∈ J ∧ B ∈ J ∧ Algsuperdiff.Section3.Provider.Whitney.CubeTouch A B
Instances For
The connected component of Q inside J.
Equations
Instances For
"𝒞 intersects layer n".