Coarse-graining support:

Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.RefinedProbeMoments

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

Refined probe moments at a good scale

The coarse probe moment bounds in QuadraticProbeBounds dominate every probe by one scalar times Λ + λ⁻¹. For the final good-scale variance estimate we need the matched form: upper coordinates cost only the upper unit-scale factor and lower coordinates cost only the lower inverse factor. This file supplies that local refinement and compresses it to \widetilde\Theta_0 using the two good-scale scalar hypotheses.

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbeUpperCoeffAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℕ) : BlockCoord d → ℝ

Upper unit-scale coefficient carried by a coordinate probe after normalization at scale m. It is nonzero only on the upper block.

Equations

• HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbeUpperCoeffAtScale hP hStruct m (Sum.inl val) = (hP.barSigmaAtScale hStruct ↑m)⁻¹
• HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbeUpperCoeffAtScale hP hStruct m (Sum.inr val) = 0

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbeLowerCoeffAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℕ) : BlockCoord d → ℝ

Lower unit-scale coefficient carried by a coordinate probe after normalization at scale m. It is nonzero only on the lower block.

Equations

• HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbeLowerCoeffAtScale hP hStruct m (Sum.inl val) = 0
• HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbeLowerCoeffAtScale hP hStruct m (Sum.inr val) = hP.barSigmaStarAtScale hStruct ↑m

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbeUpperCoeffAtScale_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (α : BlockCoord d) : 0 ≤ coordinateProbeUpperCoeffAtScale hP hStruct m α

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbeLowerCoeffAtScale_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (α : BlockCoord d) : 0 ≤ coordinateProbeLowerCoeffAtScale hP hStruct m α

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedQuadraticObservable_coordinateProbe_abs_le_weighted_factors_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (α : BlockCoord d) : (fun (a : RegCoeffField d) => |normalizedQuadraticObservable hP hStruct (↑m) (fullBlockCoordinateProbe α) (cubeSet (originCube d 0)) a.toFun|) ≤ᵐ[P] fun (a : RegCoeffField d) => coordinateProbeUpperCoeffAtScale hP hStruct m α * Ch04.LambdaSqCoeffField (originCube d 0) hP4.sUpper (Ch02.MultiscaleExponent.finite 1) a + coordinateProbeLowerCoeffAtScale hP hStruct m α * (Ch04.lambdaSqCoeffField (originCube d 0) hP4.sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹

Matched pointwise domination for coordinate probes: upper coordinates see only the upper unit-scale factor, lower coordinates only the lower inverse factor.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedQuadraticObservable_plusProbe_abs_le_weighted_factors_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) {α β : BlockCoord d} (hαβ : α ≠ β) : (fun (a : RegCoeffField d) => |normalizedQuadraticObservable hP hStruct (↑m) (fullBlockPlusProbe α β) (cubeSet (originCube d 0)) a.toFun|) ≤ᵐ[P] fun (a : RegCoeffField d) => 2 * (coordinateProbeUpperCoeffAtScale hP hStruct m α + coordinateProbeUpperCoeffAtScale hP hStruct m β) * Ch04.LambdaSqCoeffField (originCube d 0) hP4.sUpper (Ch02.MultiscaleExponent.finite 1) a + 2 * (coordinateProbeLowerCoeffAtScale hP hStruct m α + coordinateProbeLowerCoeffAtScale hP hStruct m β) * (Ch04.lambdaSqCoeffField (originCube d 0) hP4.sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹

Matched pointwise domination for plus probes.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedQuadraticObservable_minusProbe_abs_le_weighted_factors_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) {α β : BlockCoord d} (hαβ : α ≠ β) : (fun (a : RegCoeffField d) => |normalizedQuadraticObservable hP hStruct (↑m) (fullBlockMinusProbe α β) (cubeSet (originCube d 0)) a.toFun|) ≤ᵐ[P] fun (a : RegCoeffField d) => 2 * (coordinateProbeUpperCoeffAtScale hP hStruct m α + coordinateProbeUpperCoeffAtScale hP hStruct m β) * Ch04.LambdaSqCoeffField (originCube d 0) hP4.sUpper (Ch02.MultiscaleExponent.finite 1) a + 2 * (coordinateProbeLowerCoeffAtScale hP hStruct m α + coordinateProbeLowerCoeffAtScale hP hStruct m β) * (Ch04.lambdaSqCoeffField (originCube d 0) hP4.sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹

Matched pointwise domination for minus probes.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbe_centeredOrigin_momentRoot_le_widetildeTheta_of_good {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (m : ℕ) (hgood_upper : hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m) (hgood_lower : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑m)⁻¹) (α : BlockCoord d) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |Ch04.restrictionCenteredOriginObservable P 0 (fullBlockNormalizedQuadraticObservableR hP hStruct (↑m) (fullBlockCoordinateProbe α)) a| ^ hP4.xi) P ∧ (Ch04.annealedMomentRoot P hP4.xi fun (a : RegCoeffField d) => |Ch04.restrictionCenteredOriginObservable P 0 (fullBlockNormalizedQuadraticObservableR hP hStruct (↑m) (fullBlockCoordinateProbe α)) a|) ≤ 2 * ((1 + delta) * widetildeThetaAtScale P 0 hP4)

Centered origin moment for coordinate probes, compressed to \widetilde\Theta_0 by the good-scale hypotheses.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.plusProbe_centeredOrigin_momentRoot_le_widetildeTheta_of_good {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (m : ℕ) (hgood_upper : hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m) (hgood_lower : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑m)⁻¹) {α β : BlockCoord d} (hαβ : α ≠ β) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |Ch04.restrictionCenteredOriginObservable P 0 (fullBlockNormalizedQuadraticObservableR hP hStruct (↑m) (fullBlockPlusProbe α β)) a| ^ hP4.xi) P ∧ (Ch04.annealedMomentRoot P hP4.xi fun (a : RegCoeffField d) => |Ch04.restrictionCenteredOriginObservable P 0 (fullBlockNormalizedQuadraticObservableR hP hStruct (↑m) (fullBlockPlusProbe α β)) a|) ≤ 8 * ((1 + delta) * widetildeThetaAtScale P 0 hP4)

Centered origin moment for plus probes, compressed to \widetilde\Theta_0 by the good-scale hypotheses.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.minusProbe_centeredOrigin_momentRoot_le_widetildeTheta_of_good {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (m : ℕ) (hgood_upper : hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m) (hgood_lower : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑m)⁻¹) {α β : BlockCoord d} (hαβ : α ≠ β) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |Ch04.restrictionCenteredOriginObservable P 0 (fullBlockNormalizedQuadraticObservableR hP hStruct (↑m) (fullBlockMinusProbe α β)) a| ^ hP4.xi) P ∧ (Ch04.annealedMomentRoot P hP4.xi fun (a : RegCoeffField d) => |Ch04.restrictionCenteredOriginObservable P 0 (fullBlockNormalizedQuadraticObservableR hP hStruct (↑m) (fullBlockMinusProbe α β)) a|) ≤ 8 * ((1 + delta) * widetildeThetaAtScale P 0 hP4)

Centered origin moment for minus probes, compressed to \widetilde\Theta_0 by the good-scale hypotheses.