Coarse-graining support:

Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.EllipticityMoments

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

Ellipticity positive-excess moments for the coarse-fluctuation lemma

This file contains the internal Holder conversion for the lower and upper positive-excess ellipticity factors appearing in the third Section 5.3 lemma.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.holderConjugate_xi_section53CoarseFluctuationZeta {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : (↑hP4.xi).HolderConjugate (section53CoarseFluctuationZeta hP4)

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.memLp_of_integrable_nonneg_nat_pow {d : ℕ} {P : Ch04.RestrictionCoeffLaw d} {ξ : ℕ} {X : RegCoeffField d → ℝ} (hξ : 0 < ξ) (hX_aemeas : AEMeasurable X P) (hX_nonneg : ∀ᵐ (a : RegCoeffField d) ∂P, 0 ≤ X a) (hX_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => X a ^ ξ) P) : MeasureTheory.MemLp X (ENNReal.ofReal ↑ξ) P

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.shiftedUpperDecay_le_betaDecay {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) : have β := section53CoarseFluctuationBeta hP4; Real.rpow 3 (-(hP4.sUpper + β - ↑d / ↑hP4.xi) * ↑m) ≤ Real.rpow 3 (-β * ↑m)

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.shiftedLowerDecay_le_betaDecay {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) : have β := section53CoarseFluctuationBeta hP4; Real.rpow 3 (-(hP4.sLower + β - ↑d / ↑hP4.xi) * ↑m) ≤ Real.rpow 3 (-β * ↑m)

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section52MomentLossCoeff_nonneg_at_shift {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {s r : ℝ} (_hs : 0 < s) (_hsr : s < r) (hr : r < 1) : 0 ≤ section52MomentLossCoeff d hP4.xi s r

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.sq_beta_weighted_sqrt_responseDefectAverageAtScale_le_childResponseAverageAtScale {d : ℕ} [NeZero d] {a : RegCoeffField d} (ha : Ch04.AELocallyUniformlyEllipticField a) {k m : ℤ} (_hk_nonneg : 0 ≤ k) (hkm : k ≤ m) {β : ℝ} (hβ : 0 < β) (hβ_le : β ≤ 1) (p q : Vec d) : (∑ n ∈ Finset.Icc (k + 1) m, Real.rpow 3 (-β * ↑(m - n).toNat) * √(WeakNormsMaximizer.responseDefectAverageAtScale m n p q a)) ^ 2 ≤ (5 * β⁻¹) ^ 2 * descendantsAverage (originCube d m) (m - k).toNat fun (R : TriadicCube d) => Ch04.restrictionResponseJObservableCubeSet R p q a

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.lowerPositiveExcess_responseJ_expectation_le_of_integrable {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (k m : ℕ) (e : Vec d) (hLowerPowInt : have β := section53CoarseFluctuationBeta hP4; have rLower := hP4.sLower + β; MeasureTheory.Integrable (fun (a : RegCoeffField d) => max ((Ch04.lambdaSqCoeffField (originCube d ↑m) rLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹ - (hP.barSigmaStarAtScale hStruct 0)⁻¹) 0 ^ hP4.xi) P) (hResponsePowInt : have ζ := section53CoarseFluctuationZeta hP4; have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; MeasureTheory.Integrable (fun (a : RegCoeffField d) => (Ch04.restrictionResponseJObservableCubeSet (originCube d ↑k) p_e q_e a).rpow ζ) P) : have β := section53CoarseFluctuationBeta hP4; have rLower := hP4.sLower + β; have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; ∫ (a : RegCoeffField d), max ((Ch04.lambdaSqCoeffField (originCube d ↑m) rLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹ - (hP.barSigmaStarAtScale hStruct 0)⁻¹) 0 * Ch04.restrictionResponseJObservableCubeSet (originCube d ↑k) p_e q_e a ∂P ≤ lambdaInvPositiveExcessMomentAtScale P (↑m) rLower hP4.xi hP hStruct * coarseFluctuationResponseMomentAtScale hP hStruct hP4 k m e

Holder conversion for the lower inverse ellipticity positive-excess term.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.upperPositiveExcess_responseJ_expectation_le_of_integrable {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (k m : ℕ) (e : Vec d) (hUpperPowInt : have β := section53CoarseFluctuationBeta hP4; have rUpper := hP4.sUpper + β; MeasureTheory.Integrable (fun (a : RegCoeffField d) => max (Ch04.LambdaSqCoeffField (originCube d ↑m) rUpper (Ch02.MultiscaleExponent.finite 1) a - hP.barSigmaAtScale hStruct 0) 0 ^ hP4.xi) P) (hResponsePowInt : have ζ := section53CoarseFluctuationZeta hP4; have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; MeasureTheory.Integrable (fun (a : RegCoeffField d) => (Ch04.restrictionResponseJObservableCubeSet (originCube d ↑k) p_e q_e a).rpow ζ) P) : have β := section53CoarseFluctuationBeta hP4; have rUpper := hP4.sUpper + β; have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; ∫ (a : RegCoeffField d), max (Ch04.LambdaSqCoeffField (originCube d ↑m) rUpper (Ch02.MultiscaleExponent.finite 1) a - hP.barSigmaAtScale hStruct 0) 0 * Ch04.restrictionResponseJObservableCubeSet (originCube d ↑k) p_e q_e a ∂P ≤ LambdaPositiveExcessMomentAtScale P (↑m) rUpper hP4.xi hP hStruct * coarseFluctuationResponseMomentAtScale hP hStruct hP4 k m e

Holder conversion for the upper ellipticity positive-excess term.