Coarse-graining support:

Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.PositiveExcessResponseDefect

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

Positive-excess response-defect estimates

This proof-internal file contains the positive-excess estimates whose response side is a child-response average or the weighted response-defect square sum. The Holder/P4 source estimates remain in EllipticityMoments.lean.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.ellipticityPositiveExcess_childResponseAverage_expectation_le_uniform {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P), Ch04.RestrictionStationaryLaw P → ∀ (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → ∀ {k m : ℕ}, k < m → ∀ (e : Vec d), have β := section53CoarseFluctuationBeta hP4; have rLower := hP4.sLower + β; have rUpper := hP4.sUpper + β; have σ := sigmaHatAtScale hP hStruct ↑m; have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; have childAvg := fun (a : RegCoeffField d) => descendantsAverage (originCube d ↑m) (↑m - ↑k).toNat fun (R : TriadicCube d) => Ch04.restrictionResponseJObservableCubeSet R p_e q_e a; σ * ∫ (a : RegCoeffField d), max ((Ch04.lambdaSqCoeffField (originCube d ↑m) rLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹ - (hP.barSigmaStarAtScale hStruct 0)⁻¹) 0 * childAvg a ∂P + σ⁻¹ * ∫ (a : RegCoeffField d), max (Ch04.LambdaSqCoeffField (originCube d ↑m) rUpper (Ch02.MultiscaleExponent.finite 1) a - hP.barSigmaAtScale hStruct 0) 0 * childAvg a ∂P ≤ C * ↑hP4.xi * Real.rpow 3 (-β * ↑m) * coarseFluctuationUnitMomentWeightAtScale hP hStruct hP4 m * coarseFluctuationResponseMomentAtScale hP hStruct hP4 k m e