SuperposedConclusion #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The corrected superposed competitor in the Section 3 conclusion #
This file performs the deterministic composition at the superposed affine competitor. Its two fields are deliberately different:
F = superposedCompetitorSlope ... p, the slope field of the superposed scalar competitor;G = superposedCompetitorDivergence ... q, the divergence of the antisymmetric matrix assembled from the basis-load scalar competitors.
In particular, the G leg is never the slope construction rerun at q.
The first theorem is the exact conditional e.sum-of-a-decomp seam. The
second composes it with the already assembled Step-3 payload, using the common
collar constant superposedDivConst d. The smaller F-leg constant is
weakened by superposedGradConst_le_superposedDivConst; the G-leg envelope
is the one proved in Affine.SuperposedDivergence.
The exact conditional decomposition seam #
theorem
Algsuperdiff.Section3.Provider.Multiscale.ofReal_abs_blockVecDot_le_tsum_superposedDivergence
{d : ℕ}
{M : ABKModel d}
{m : ℤ}
{E b : ℝ}
{k₀ : ℕ}
{omega : Cutoff.CutoffSample d}
(hd : 2 ≤ d)
(hb0 : 0 < b)
(hb : b ≤ 1 / 8)
(hk₀ : 3 ≤ k₀)
(hne : (Percolation.hsepSet M m E b omega).Nonempty)
(L : ℤ)
(p q : HCPolySupport.Vec d)
(hF :
HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))
fun (x : HCPolySupport.Vec d) =>
Affine.superposedCompetitorSlope m (Whitney.whitneyScale M m E b k₀ omega)
(Whitney.badFamily M m (Whitney.whitneyScale M m E b k₀ omega) omega) p x - p)
(hG :
HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))
fun (x : HCPolySupport.Vec d) =>
Affine.superposedCompetitorDivergence m (Whitney.whitneyScale M m E b k₀ omega)
(Whitney.badFamily M m (Whitney.whitneyScale M m E b k₀ omega) omega) q x - q)
:
ENNReal.ofReal
|HCPolySupport.blockVecDot (p, q)
(HCPolySupport.blockMatVecMul
(HCPolySupport.Book.Ch02.coarseBlockMatrix (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d m))
((Cutoff.coefficientCutoffTriadicCoeffFamily M L omega).coeffOn (HCPolySupport.originCube d m)))
(p, q))| ≤ ∑' (T : ↑(Whitney.simplexPartition m (Whitney.whitneyScale M m E b k₀ omega))), (ENNReal.ofReal (cellWeight m ↑T * goodCellForm M m (Whitney.whitneyScale M m E b k₀ omega) L omega p q ↑T) + ENNReal.ofReal
(cellWeight m ↑T * collarCellForm M m (Whitney.whitneyScale M m E b k₀ omega) L omega
(Affine.superposedCompetitorCellSlope m (Whitney.whitneyScale M m E b k₀ omega)
(Whitney.badFamily M m (Whitney.whitneyScale M m E b k₀ omega) omega) p)
(Affine.superposedCompetitorCellDivergence m (Whitney.whitneyScale M m E b k₀ omega)
(Whitney.badFamily M m (Whitney.whitneyScale M m E b k₀ omega) omega) q)
↑T))
The e.sum-of-a-decomp inequality at the corrected superposed pair.
The only analytic premises are the two manuscript Sobolev memberships, stated at the actual global fields consumed by the decomposition. All cellwise constancy, bad-cell vanishing, and off-collar normalization clauses are discharged by the proved superposed slope and divergence A.
theorem
Algsuperdiff.Section3.Provider.Multiscale.ofReal_abs_blockVecDot_le_tsum_superposedDivergence_of_forall
{d : ℕ}
{M : ABKModel d}
{m : ℤ}
{E b : ℝ}
{k₀ : ℕ}
{omega : Cutoff.CutoffSample d}
(hd : 2 ≤ d)
(hb0 : 0 < b)
(hb : b ≤ 1 / 8)
(hk₀ : 3 ≤ k₀)
(hne : (Percolation.hsepSet M m E b omega).Nonempty)
(L : ℤ)
(p q : HCPolySupport.Vec d)
(hF :
∀ (r : HCPolySupport.Vec d),
HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))
fun (x : HCPolySupport.Vec d) =>
Affine.superposedCompetitorSlope m (Whitney.whitneyScale M m E b k₀ omega)
(Whitney.badFamily M m (Whitney.whitneyScale M m E b k₀ omega) omega) r x - r)
:
ENNReal.ofReal
|HCPolySupport.blockVecDot (p, q)
(HCPolySupport.blockMatVecMul
(HCPolySupport.Book.Ch02.coarseBlockMatrix (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d m))
((Cutoff.coefficientCutoffTriadicCoeffFamily M L omega).coeffOn (HCPolySupport.originCube d m)))
(p, q))| ≤ ∑' (T : ↑(Whitney.simplexPartition m (Whitney.whitneyScale M m E b k₀ omega))), (ENNReal.ofReal (cellWeight m ↑T * goodCellForm M m (Whitney.whitneyScale M m E b k₀ omega) L omega p q ↑T) + ENNReal.ofReal
(cellWeight m ↑T * collarCellForm M m (Whitney.whitneyScale M m E b k₀ omega) L omega
(Affine.superposedCompetitorCellSlope m (Whitney.whitneyScale M m E b k₀ omega)
(Whitney.badFamily M m (Whitney.whitneyScale M m E b k₀ omega) omega) p)
(Affine.superposedCompetitorCellDivergence m (Whitney.whitneyScale M m E b k₀ omega)
(Whitney.badFamily M m (Whitney.whitneyScale M m E b k₀ omega) omega) q)
↑T))
One-premise form of the corrected decomposition seam. An all-load
potential theorem supplies the F leg at p; its basis-load specializations
produce the correct solenoidal G leg through the antisymmetric-divergence
bridge.
Composition with the assembled payload #
theorem
Algsuperdiff.Section3.Provider.Multiscale.abs_blockVecDot_coarseBlockMatrix_originCube_le_payload_superposedDivergence_ae
{d : ℕ}
(hd : 2 ≤ d)
(M : ABKModel d)
{m0 : ℤ}
{E : { E : ℝ // 1 ≤ E }}
(hS : Frozen.Section3.inductionState M m0 E)
(m : ℤ)
{b : ℝ}
(hb0 : 0 < b)
(hb : b ≤ 1 / 8)
{k₀ : ℕ}
(hk₀ : 3 ≤ k₀)
{i : ℤ}
(hmi : m - 1 ≤ i)
(hi : i ≤ m0)
{L : ℤ}
(hmL : m ≤ L)
(p q : HCPolySupport.Vec d)
{eps : ℝ}
(heps : 0 < eps)
{t : ℝ}
(ht0 : 0 ≤ t)
{beta : ℝ}
(hbeta0 : 0 < beta)
(hbeta9 : 9 * beta ≤ 1)
(hbetab : 2 * b + 2 * M.gamma + eps ≤ 2 * beta)
(hgammaWin : 4 * (2 * M.gamma + eps) ≤ 1 - beta)
{kp : ℕ}
(hcap :
9 * 99 ^ d * (Real.exp (-(Percolation.siteRateBase d / 2 * ((↑E)⁻¹ ^ 2 * M.gamma⁻¹))) + 3 ^ (-(↑k₀ / 2))) ≤ Real.exp (-↑kp))
:
∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), (Percolation.hsepSet M m (↑E) b omega).Nonempty →
(∀ (n : ℕ),
∀ Q ∈ Whitney.whitneyLayer m (Whitney.whitneyScale M m (↑E) b k₀ omega) n,
Stream.cubeSupBound Q Q.scale L ↑omega ≤ whitneyWaveLayerScale M m (Whitney.whitneyScale M m (↑E) b k₀ omega) n L * t) →
(HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))
fun (x : HCPolySupport.Vec d) =>
Affine.superposedCompetitorSlope m (Whitney.whitneyScale M m (↑E) b k₀ omega)
(Whitney.badFamily M m (Whitney.whitneyScale M m (↑E) b k₀ omega) omega)
((√↑(Annealed.sigmaBar M i))⁻¹ • p) x - (√↑(Annealed.sigmaBar M i))⁻¹ • p) →
(HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn
(HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (x : HCPolySupport.Vec d) =>
Affine.superposedCompetitorDivergence m (Whitney.whitneyScale M m (↑E) b k₀ omega)
(Whitney.badFamily M m (Whitney.whitneyScale M m (↑E) b k₀ omega) omega) (√↑(Annealed.sigmaBar M i) • q)
x - √↑(Annealed.sigmaBar M i) • q) →
|HCPolySupport.blockVecDot ((√↑(Annealed.sigmaBar M i))⁻¹ • p, √↑(Annealed.sigmaBar M i) • q)
(HCPolySupport.blockMatVecMul
(HCPolySupport.Book.Ch02.coarseBlockMatrix
(HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d m))
((Cutoff.coefficientCutoffTriadicCoeffFamily M L omega).coeffOn (HCPolySupport.originCube d m)))
((√↑(Annealed.sigmaBar M i))⁻¹ • p, √↑(Annealed.sigmaBar M i) • q))| ≤ layerSumConst beta (2 * M.gamma + eps) kp (ktotConst M m i 3 (ktotEnvelopeSup M m L eps t) p q)
(collarEnvelopeConst M m i L eps t (Affine.superposedDivConst d) p q) (6 * ↑d) * (3 ^ ((2 * M.gamma + eps) * ↑(Percolation.hsep M m (↑E) b omega + k₀)) * (1 + 3 ^ (2 * beta * ↑(Percolation.hsep M m (↑E) b omega + k₀)) * Real.exp (-(↑kp / 36))))
The corrected superposed branch of the Step-3 conclusion, conditional only
on the two global Sobolev memberships. Both collar legs are priced with the
common constant superposedDivConst d; this is exact for G and a monotone
weakening of the superposedGradConst d estimate for F.