CombineFiniteTwoChannel #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Quantitative descendant channel #
This module assembles the finite quadratic probes of the relative descendant
fluctuation matrix. The observation cube is at physical scale n, while its
relative centre is n - L - c and its children end at the fixed relative scale
-c.
theorem
Algsuperdiff.Section3.Provider.Homogenization.two_mul_integral_relativeStarredDescendantOperatorNormSq_le
{d : ℕ}
[NeZero d]
(M : ABKModel d)
(L n : ℤ)
(hLn : L ≤ n)
{s A D : ℝ}
(hs : 0 < s)
(hLower :
Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2)
(HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Observable.cutoffHomogenizationError M L ⟨s, hs⟩) A D)
:
have c := ↑(Cutoff.cutoffRelativeNormalizationShift d);
have P := Cutoff.relativeNormalizedCutoffLaw M L;
have hP := ⋯;
have hStruct := ⋯;
have center := n - L - c;
have Q := HCPolySupport.originCube d center;
have j := (n - L).toNat;
have sigma := Annealed.sigmaBar M L;
have a0 := Observable.isotropicComparatorMatrix sigma;
have B := HCPolySupport.Book.Ch02.constantFullBlockMatrix a0;
have Cn := HCPolySupport.Book.Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct center;
have N := ↑(HCPolySupport.descendantsAtScale Q (-c)).card;
have card := ↑(Fintype.card (HCPolySupport.BlockCoord d));
have budget :=
2 * ((HCPolySupport.IndependentSums.gammaMomentConst 2 * 2 ^ 2⁻¹ * A) ^ 2 + (HCPolySupport.IndependentSums.gammaMomentConst (1 / 2) * 2 ^ (1 / 2)⁻¹ * D) ^ 2) + 8 * ((HCPolySupport.IndependentSums.gammaMomentConst 2 * 4 ^ 2⁻¹ * A) ^ 4 + (HCPolySupport.IndependentSums.gammaMomentConst (1 / 2) * 4 ^ (1 / 2)⁻¹ * D) ^ 4);
have secondBudget :=
2 * ((HCPolySupport.IndependentSums.gammaMomentConst 2 * 2 ^ 2⁻¹ * A) ^ 2 + (HCPolySupport.IndependentSums.gammaMomentConst (1 / 2) * 2 ^ (1 / 2)⁻¹ * D) ^ 2);
have probeRhs := fun (q : HCPolySupport.FullBlockVec d) =>
have probeBudget := 6 * (q ⬝ᵥ q) ^ 2 * budget;
have meanBudget := 4 * (q ⬝ᵥ q) ^ 2 * secondBudget ^ 2;
have K := √probeBudget;
have rootBound :=
N⁻¹ * (HCPolySupport.Book.Ch04.rosenthalDescendantsAtScaleLpConst d (-c) 2 * N ^ (1 / 2) * K + HCPolySupport.Book.Ch04.rosenthalDescendantsAtScaleSqrtConst d (-c) 2 * √N * K);
2 * rootBound ^ 2 + 2 * meanBudget;
MeasureTheory.Integrable (starredDescendantsAverageFluctuationOperatorNormSq B Cn Q j) P ∧ 2 * ∫ (a : HCPolySupport.RegCoeffField d), starredDescendantsAverageFluctuationOperatorNormSq B Cn Q j a ∂P ≤ 2 * card ^ 2 * (card * ∑ alpha : HCPolySupport.BlockCoord d,
card * ∑ beta : HCPolySupport.BlockCoord d,
3 * (probeRhs (HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockCoordinateProbe alpha) + probeRhs (HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockPlusProbe alpha beta) + probeRhs (HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockMinusProbe alpha beta)))
The finite-coordinate reconstruction of the relative descendant operator norm. Its right side records the exact probe bounds used by the downstream quantitative variance assembly.