ShellActiveSigma #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Independence of local functionals read at index-dependent truncation levels #
Why a level-uniform producer is not enough #
The proved cross-shell and spatial-range results fix one truncation index
for the whole family:
Cutoff.indep_lowerShellLocalCompletion_of_cutoff_separation compares two
observation regions read by the same cutoff k_m, and asks for the
separation threshold sqrt d * 3 ^ m. ABK26's Section 4.1 atoms are not of
that shape. The G_0 atom
Y_n = gamma^{-4} sum_{k <= n} 3^{-gamma(n-k)/4}
max_{z in 3^{k-2} Z^d cap (Box_n \ Box_{n-1})}
( sigmabar_{k-3} * lambda_{gamma,2}^{-1}(z + Box_{k-2}; a_{k-2}) - C )_+
reads the field a_{n-2} on the annulus Box_n \ Box_{n-1}: both the read
region and the truncation level move with the index, Lidx n = n - 2. At a
fixed level L the separation hypothesis of a level-uniform producer is
unsatisfiable -- annuli far below L have diameter much smaller than
sqrt d * 3 ^ L.
The true geometry and the mechanism #
For n' < n the shells n' - 2 < i <= n - 2 are read by Y_n alone and
drop out for free by the cross-shell independence of ABK26 -- at any
spatial position. Only the shared shells i <= n' - 2 need decorrelating,
and their range of dependence is sqrt d * 3 ^ (n' - 2) = sqrt d * 3 ^ (min (Lidx n) (Lidx n')). Hence the honest separation
threshold is
sqrt d * 3 ^ (min (Lidx i) (Lidx j))
which the annuli do satisfy. This module proves the independence statement at exactly that threshold.
The carrier translation #
On this repository's carriers the bi-infinite truncation floor is -infinity
rather than a finite L_0: the genuine cutoff Cutoff.cutoff m sums all
shells at or below m. Consequently the per-index join of the per-shell read
sigma-fields collapses onto a proved object,
sup over l of (activeShellSigma Lidx U i l) >= lowerShellLocalSigma (Lidx i) (U i),
and the varying-level producer is exactly the statement that the family
(lowerShellLocalSigma (Lidx i) (U i))_i is mutually independent. The
row decomposition indexed by the shell l is still needed -- it is what feeds
iIndep_iSup_of_iIndep_rows -- so activeShellRegion / activeShellSigma are
kept as the per-(index, shell) read region and its sigma-field.
- the local information of a shell is CoarseGraining's integral-generated
Homogenization.LocalSigmaR, pulled back byFrozen.Assumptions.ShellField.lihLocalSigma, not a point-value restriction sigma-field; it takes no measurability argument, soactiveShellSigmaneeds none either; - the genuine lower-infinite cutoff is only an almost-everywhere limit of its
finite truncations, so the statement usable by Section 4 lives on the
completed sigma-field
Cutoff.lowerShellLocalCompletionand, after transport through the full-measure subtype, onCutoff.cutoffSampleLocalSigma. The completion and subtype steps mirror the proved two-set resultsCutoff.indep_lowerShellLocalCompletion_of_indepandCutoff.indep_cutoffSampleLocalSigma_of_indep_completionin the mutual (iIndep) form.
Main definitions #
SeparatedBy: two regions at Euclidean distance at leastr, in the exact spelling consumed byFrozen.Assumptions.ShellLawJ1.range_dependence.activeShellRegion,activeShellSigma: the region indexireads of shelll, and the sigma-field it generates.
Main results #
iIndep_shellLocalSigma_of_pairwise_separated: at one shell, pairwise separated regions generate mutually independent local sigma-fields.iIndep_activeShellSigma_row: the row statement at the honest threshold.iIndep_lowerShellLocalSigma_of_varyingLevel: the producer, sigma-field form on the shell sequence.iIndep_cutoffSampleLocalSigma_of_varyingLevel: the producer on the genuine cutoff carrier.iIndepFun_of_local_cutoffSample: the producer, observable form.
Separation in the manuscript's metric #
Two observation regions are r-separated: every pair of points is at Euclidean
distance at least r. This is the exact predicate carried by
ShellLawJ1.range_dependence and by the proved cutoff-range results.
Equations
- Algsuperdiff.Section4.Probability.SeparatedBy r U V = ∀ ⦃x y : HCPolySupport.Vec d⦄, x ∈ U → y ∈ V → r ≤ HCPolySupport.Book.Ch02.vecNorm (x - y)
Instances For
Auxiliary monotonicity and almost-everywhere bookkeeping #
Mutual independence at one shell #
Pairwise separation gives mutual independence at one shell. This is the
iIndep form of the proved two-set result
Cutoff.indep_shellLocal_of_cutoff_separation: the two-set statement is
applied to one region against the union of the remaining ones along a Finset
induction, which is legitimate because the local sigma-field is monotone in the
region.
The per-(index, shell) read region #
The read region of index i at shell l. Index i truncates at level
Lidx i, so it reads shell l only when l ≤ Lidx i; there it reads U i,
and elsewhere nothing.
Equations
Instances For
The (index, shell) sigma-field: what index i can see of shell l.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The (index, shell) sigma-field is contained in the whole information of
shell l.
The varying-level locality, in the direction the producer needs. Every
shell at or below Lidx i is read on U i, so the proved lower-shell local
sigma-field of index i sits inside the single join of its (index, shell)
sigma-fields.
The producer #
Row independence at a fixed shell. For each shell l the family of
(index, shell) sigma-fields is mutually independent.
The regions active at l are pairwise (sqrt d * 3 ^ l)-separated: if both i
and j read shell l then l ≤ Lidx i and l ≤ Lidx j, hence
l ≤ min (Lidx i) (Lidx j) and the hypothesis supplies the larger threshold
sqrt d * 3 ^ min; if either is inactive its region is empty and separation is
vacuous.
The producer, sigma-field form on the shell sequence. At the honest
threshold sqrt d * 3 ^ (min (Lidx i) (Lidx j)), the lower-shell local
sigma-fields read at the index-dependent levels Lidx i are mutually
independent.
The cross-shell assumption of ABK26 supplies the mutual independence of the shells;
iIndep_activeShellSigma_row supplies each row; iIndep_iSup_of_iIndep_rows assembles
the joins, and each join dominates the corresponding lower-shell local sigma-field.
Mutual independence survives completion by ambient null sets. The genuine
lower-infinite cutoff is measurable only for the completed lower-shell
sigma-field, so this is the form in which the varying-level producer can be
consumed. It is the mutual analogue of the proved two-set result
Cutoff.indep_lowerShellLocalCompletion_of_indep.
The producer, sigma-field form on the genuine cutoff carrier. The
completed statement descends faithfully to the full-measure cutoff subtype
through Borel local representatives, so no containment of a completion in the
ambient Borel sigma-field is claimed. This is the mutual analogue of the
proved two-set result
Cutoff.indep_cutoffSampleLocalSigma_of_indep_completion.
The producer on the genuine cutoff carrier, assembled from the honest separation geometry alone.
The producer, observable form. Real observables of the genuine cutoff sample that
are local in U i and read only truncations at or below their own level Lidx i are mutually independent, provided the observation regions are pairwise
separated at the honest threshold sqrt d * 3 ^ (min (Lidx i) (Lidx j)).
The atom Phi i is an arbitrary functional of the whole sample that is
measurable for cutoffSampleLocalSigma M (Lidx i) (U i); it may therefore read
every truncation k_{L'} with L' ≤ Lidx i, each only on U i, which is
exactly what ABK26's atoms do (ABK26: one truncation per inner scale).