Coarse-graining support: Support.Book.Ch05.Theorems.Section52.FluctuationBridge

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Section 5.2 internals: FluctuationBridge

Pointwise fluctuation bridges for positive-excess bounds.

theorem HCPolySupport.Book.Ch05.Section52.finsetSupReal_eq_sup' {α : Type u_1} (s : Finset α) (hs : s.Nonempty) (f : α → ℝ) : Ch02.finsetSupReal s f = s.sup' hs f

theorem HCPolySupport.Book.Ch05.Section52.maxDescendantBMatrixNorm_eq_sup_upperLeft_of_uniformEllipticity {d : ℕ} [NeZero d] {a : RegCoeffField d} (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) : Ch04.maxDescendantBMatrixNormCoeffFieldAtScale Q k a = (descendantsAtScale Q k).sup' ⋯ fun (R : TriadicCube d) => Ch02.matrixNorm (coarseBlockMatrix (cubeSet R) a.toFun).upperLeft

theorem HCPolySupport.Book.Ch05.Section52.maxDescendantSigmaStarInvMatrixNormCoeffField_eq_sup_lowerRight {d : ℕ} [NeZero d] {a : RegCoeffField d} (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) : Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale Q k a = (descendantsAtScale Q k).sup' ⋯ fun (R : TriadicCube d) => Ch02.matrixNorm (coarseBlockMatrix (cubeSet R) a.toFun).lowerRight

theorem HCPolySupport.Book.Ch05.Section52.matrixNorm_smul_one_eq_of_nonneg {d : ℕ} [NeZero d] {c : ℝ} (hc : 0 ≤ c) : Ch02.matrixNorm (c • 1) = c

theorem HCPolySupport.Book.Ch05.Section52.upperLargeScaleRaw_sum_le_base_add_positiveExcess_sum {d : ℕ} [NeZero d] (m : ℕ) {s base : ℝ} (hs : 0 < s) (hbase : 0 ≤ base) (a : RegCoeffField d) : ∑ n ∈ section52LargeScaleSet m, section52LargeScaleWeight s m n * Ch04.maxDescendantBMatrixNormCoeffFieldAtScale (originCube d ↑m) n a ≤ base + ∑ n ∈ (section52LargeScaleSet m).attach, section52LargeScaleWeight s m ↑n * let parents := descendantsAtScale (originCube d ↑m) ↑n; have hparents := ⋯; parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft - Ch02.matrixNorm (base • 1)) 0

theorem HCPolySupport.Book.Ch05.Section52.upperPositiveExcess_pointwise_le_smallTail_add_largeScalePositiveExcess {d : ℕ} [NeZero d] (m : ℕ) {s base : ℝ} (hs : 0 < s) (hbase : 0 ≤ base) (a : RegCoeffField d) : max (Ch04.LambdaSqCoeffField (originCube d ↑m) s (Ch02.MultiscaleExponent.finite 1) a - base) 0 ≤ upperSmallSqrtTailCoeffField m s a ^ 2 / section52SmallTailWeight s m + ∑ n ∈ (section52LargeScaleSet m).attach, section52LargeScaleWeight s m ↑n * let parents := descendantsAtScale (originCube d ↑m) ↑n; have hparents := ⋯; parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft - Ch02.matrixNorm (base • 1)) 0

theorem HCPolySupport.Book.Ch05.Section52.lowerLargeScaleRaw_sum_le_base_add_positiveExcess_sum {d : ℕ} [NeZero d] (m : ℕ) {s base : ℝ} (hs : 0 < s) (hbase : 0 ≤ base) (a : RegCoeffField d) : ∑ n ∈ section52LargeScaleSet m, section52LargeScaleWeight s m n * Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale (originCube d ↑m) n a ≤ base + ∑ n ∈ (section52LargeScaleSet m).attach, section52LargeScaleWeight s m ↑n * let parents := descendantsAtScale (originCube d ↑m) ↑n; have hparents := ⋯; parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight - Ch02.matrixNorm (base • 1)) 0

theorem HCPolySupport.Book.Ch05.Section52.lowerPositiveExcess_pointwise_le_smallTail_add_largeScalePositiveExcess {d : ℕ} [NeZero d] (m : ℕ) {s base : ℝ} (hs : 0 < s) (hbase : 0 ≤ base) (a : RegCoeffField d) : max ((Ch04.lambdaSqCoeffField (originCube d ↑m) s (Ch02.MultiscaleExponent.finite 1) a)⁻¹ - base) 0 ≤ lowerSmallSqrtTailCoeffField m s a ^ 2 / section52SmallTailWeight s m + ∑ n ∈ (section52LargeScaleSet m).attach, section52LargeScaleWeight s m ↑n * let parents := descendantsAtScale (originCube d ↑m) ↑n; have hparents := ⋯; parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight - Ch02.matrixNorm (base • 1)) 0

theorem HCPolySupport.Book.Ch05.Section52.section52_upperCenter_entries {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (i j : Fin d) : (hP.barSigmaAtScale hStruct 0 • 1) i j = ∫ (b : RegCoeffField d), (coarseBlockMatrix (cubeSet (originCube d 0)) b.toFun).upperLeft i j ∂P

theorem HCPolySupport.Book.Ch05.Section52.section52_lowerCenter_entries {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (i j : Fin d) : ((hP.barSigmaStarAtScale hStruct 0)⁻¹ • 1) i j = ∫ (b : RegCoeffField d), (coarseBlockMatrix (cubeSet (originCube d 0)) b.toFun).lowerRight i j ∂P

theorem HCPolySupport.Book.Ch05.Section52.upperLargeScaleFiniteParentFluctuation {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {m n : ℕ} (hnm : n ≤ m) : let parents := descendantsAtScale (originCube d ↑m) ↑n; have hparents := ⋯; have K := 2 * Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi; have B := parents.sup' hparents fun (Q : TriadicCube d) => section52UnitDescendantRosenthalBudget Q hP4.xi K; (Ch04.annealedMomentRoot P hP4.xi fun (a : RegCoeffField d) => parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft - Ch02.matrixNorm (hP.barSigmaAtScale hStruct 0 • 1)) 0) ≤ ↑(Fintype.card (Fin d)) * ↑(Fintype.card (Fin d)) * (↑parents.card ^ (1 / ↑hP4.xi) * B)

theorem HCPolySupport.Book.Ch05.Section52.lowerLargeScaleFiniteParentFluctuation {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {m n : ℕ} (hnm : n ≤ m) : let parents := descendantsAtScale (originCube d ↑m) ↑n; have hparents := ⋯; have K := 2 * Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi; have B := parents.sup' hparents fun (Q : TriadicCube d) => section52UnitDescendantRosenthalBudget Q hP4.xi K; (Ch04.annealedMomentRoot P hP4.xi fun (a : RegCoeffField d) => parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight - Ch02.matrixNorm ((hP.barSigmaStarAtScale hStruct 0)⁻¹ • 1)) 0) ≤ ↑(Fintype.card (Fin d)) * ↑(Fintype.card (Fin d)) * (↑parents.card ^ (1 / ↑hP4.xi) * B)