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

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

Section 5.2 internals: PositiveExcessUpper

Upper large-scale positive-excess estimates.

theorem HCPolySupport.Book.Ch05.Section52.section52_annealedMomentRoot_const_mul_of_nonneg {d : ℕ} {P : Ch04.RestrictionCoeffLaw d} {ξ : ℕ} {c : ℝ} {X : RegCoeffField d → ℝ} (hξ : 1 ≤ ξ) (hc : 0 ≤ c) (hX_nonneg : ∀ (a : RegCoeffField d), 0 ≤ X a) : (Ch04.annealedMomentRoot P ξ fun (a : RegCoeffField d) => c * X a) = c * Ch04.annealedMomentRoot P ξ X

theorem HCPolySupport.Book.Ch05.Section52.section52_descendantsAtScale_zero_card_of_scale_eq {d : ℕ} (Q : TriadicCube d) {n : ℤ} (hn : 0 ≤ n) (hQscale : Q.scale = n) : (descendantsAtScale Q 0).card = (3 ^ d) ^ n.toNat

theorem HCPolySupport.Book.Ch05.Section52.section52UnitDescendantRosenthalBudget_eq_originCube_of_scale_eq {d : ℕ} (Q : TriadicCube d) {n : ℤ} (hn : 0 ≤ n) (hQscale : Q.scale = n) (ξ : ℕ) (K : ℝ) : section52UnitDescendantRosenthalBudget Q ξ K = section52UnitDescendantRosenthalBudget (originCube d n) ξ K

theorem HCPolySupport.Book.Ch05.Section52.upperLargeScalePositiveExcessRoot_le_largeScaleRootCoeff {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) : let parents := descendantsAtScale (originCube d ↑m) n; have hparents := ⋯; (Ch04.annealedMomentRoot P hP4.xi fun (a : RegCoeffField d) => section52LargeScaleWeight hP4.sUpper m n * 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)) * section52LargeScaleRootCoeff d hP4.xi hP4.sUpper m n * Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi

theorem HCPolySupport.Book.Ch05.Section52.upperLargeScalePositiveExcess_integrable_abs_pow {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) : let parents := descendantsAtScale (originCube d ↑m) n; have hparents := ⋯; MeasureTheory.Integrable (fun (a : RegCoeffField d) => ‖section52LargeScaleWeight hP4.sUpper m n * parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft - Ch02.matrixNorm (hP.barSigmaAtScale hStruct 0 • 1)) 0‖ ^ hP4.xi) P

theorem HCPolySupport.Book.Ch05.Section52.upperLargeScalePositiveExcess_integrable_abs_pow_source {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {sSource r : ℝ} {ξ : ℕ} (hsSource : 0 < sSource) (hξ_one : 1 ≤ ξ) (hξ_two : 2 ≤ ξ) (hUpperSourceInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.LambdaSqCoeffField (originCube d 0) sSource (Ch02.MultiscaleExponent.finite 1) a ^ ξ) P) {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) : let parents := descendantsAtScale (originCube d ↑m) n; have hparents := ⋯; MeasureTheory.Integrable (fun (a : RegCoeffField d) => ‖section52LargeScaleWeight r m n * parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft - Ch02.matrixNorm (hP.barSigmaAtScale hStruct 0 • 1)) 0‖ ^ ξ) P

theorem HCPolySupport.Book.Ch05.Section52.upperLargeScalePositiveExcess_aemeasurable {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) : let parents := descendantsAtScale (originCube d ↑m) n; have hparents := ⋯; AEMeasurable (fun (a : RegCoeffField d) => section52LargeScaleWeight hP4.sUpper m n * parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft - Ch02.matrixNorm (hP.barSigmaAtScale hStruct 0 • 1)) 0) P

theorem HCPolySupport.Book.Ch05.Section52.upperLargeScalePositiveExcess_aemeasurable_source {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {r : ℝ} {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) : let parents := descendantsAtScale (originCube d ↑m) n; have hparents := ⋯; AEMeasurable (fun (a : RegCoeffField d) => section52LargeScaleWeight r m n * parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft - Ch02.matrixNorm (hP.barSigmaAtScale hStruct 0 • 1)) 0) P

theorem HCPolySupport.Book.Ch05.Section52.upperLargeScalePositiveExcess_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) (a : RegCoeffField d) : let parents := descendantsAtScale (originCube d ↑m) n; have hparents := ⋯; 0 ≤ section52LargeScaleWeight hP4.sUpper m n * parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft - Ch02.matrixNorm (hP.barSigmaAtScale hStruct 0 • 1)) 0

theorem HCPolySupport.Book.Ch05.Section52.upperLargeScalePositiveExcess_nonneg_source {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {r : ℝ} (hr_nonneg : 0 ≤ r) {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) (a : RegCoeffField d) : let parents := descendantsAtScale (originCube d ↑m) n; have hparents := ⋯; 0 ≤ section52LargeScaleWeight r m n * parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft - Ch02.matrixNorm (hP.barSigmaAtScale hStruct 0 • 1)) 0

theorem HCPolySupport.Book.Ch05.Section52.upperLargeScalePositiveExcessRoot_le_largeScaleRootCoeff_source {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {sSource r : ℝ} {ξ : ℕ} (hsSource : 0 < sSource) (hr_nonneg : 0 ≤ r) (hξ_one : 1 ≤ ξ) (hξ_two : 2 ≤ ξ) (hUpperSourceInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.LambdaSqCoeffField (originCube d 0) sSource (Ch02.MultiscaleExponent.finite 1) a ^ ξ) P) {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) : let parents := descendantsAtScale (originCube d ↑m) n; have hparents := ⋯; (Ch04.annealedMomentRoot P ξ fun (a : RegCoeffField d) => section52LargeScaleWeight r m n * 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)) * section52LargeScaleRootCoeff d ξ r m n * Ch04.LambdaMomentAtScale P 0 sSource ξ