Coarse-graining support: Support.Book.Ch04.Theorems.PartitionAveragesDefinitions

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

Restriction-Carrier Partition-Average Fluctuation Definitions

Definitions and equality lemmas for the restriction-carrier engineering partition-average fluctuation endpoints. Source-manuscript counterparts live in the source-specific API.

noncomputable def HCPolySupport.Book.Ch04.restrictionCenteredOriginObservable {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) (X : Set (Vec d) → RegCoeffField d → ℝ) : RegCoeffField d → ℝ

The origin observable centered by its expectation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch04.restrictionDescendantAverage {d : ℕ} (n m : ℤ) (X : Set (Vec d) → RegCoeffField d → ℝ) : RegCoeffField d → ℝ

The uncentered descendant partition average over the scale-n descendants of the origin cube at scale m.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch04.restrictionCenteredDescendantAverage {d : ℕ} (P : RestrictionCoeffLaw d) (n m : ℤ) (X : Set (Vec d) → RegCoeffField d → ℝ) : RegCoeffField d → ℝ

The centered descendant partition average over the scale-n descendants of the origin cube at scale m.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch04.restrictionDescendantAverageOnCube {d : ℕ} (Q : TriadicCube d) (n : ℤ) (X : Set (Vec d) → RegCoeffField d → ℝ) : RegCoeffField d → ℝ

The uncentered descendant partition average over the scale-n descendants of an arbitrary parent cube.

Equations

• HCPolySupport.Book.Ch04.restrictionDescendantAverageOnCube Q n X a = (↑(HCPolySupport.descendantsAtScale Q n).card)⁻¹ * ∑ R ∈ HCPolySupport.descendantsAtScale Q n, X (HCPolySupport.cubeSet R) a

noncomputable def HCPolySupport.Book.Ch04.restrictionCenteredDescendantAverageOnCube {d : ℕ} (P : RestrictionCoeffLaw d) (Q : TriadicCube d) (n : ℤ) (X : Set (Vec d) → RegCoeffField d → ℝ) : RegCoeffField d → ℝ

The centered descendant partition average over the scale-n descendants of an arbitrary parent cube, centered by the origin scale-n expectation.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch04.restrictionCenteredOriginObservable_ae_eq_of_ae_eq {d : ℕ} {P : RestrictionCoeffLaw d} {n : ℤ} {X Y : Set (Vec d) → RegCoeffField d → ℝ} (hXY : X (cubeSet (originCube d n)) =ᵐ[P] Y (cubeSet (originCube d n))) : restrictionCenteredOriginObservable P n X =ᵐ[P] restrictionCenteredOriginObservable P n Y

A.e.-equal observables have the same centered origin observable.

theorem HCPolySupport.Book.Ch04.restrictionDescendantAverageOnCube_ae_eq_of_ae_eq {d : ℕ} {P : RestrictionCoeffLaw d} {Q : TriadicCube d} {n : ℤ} {X Y : Set (Vec d) → RegCoeffField d → ℝ} (hXY : ∀ R ∈ descendantsAtScale Q n, X (cubeSet R) =ᵐ[P] Y (cubeSet R)) : restrictionDescendantAverageOnCube Q n X =ᵐ[P] restrictionDescendantAverageOnCube Q n Y

A.e.-equal descendant observables have the same uncentered descendant average on a fixed parent cube.

theorem HCPolySupport.Book.Ch04.restrictionCenteredDescendantAverageOnCube_ae_eq_of_ae_eq {d : ℕ} {P : RestrictionCoeffLaw d} {Q : TriadicCube d} {n : ℤ} {X Y : Set (Vec d) → RegCoeffField d → ℝ} (hOrigin : X (cubeSet (originCube d n)) =ᵐ[P] Y (cubeSet (originCube d n))) (hDesc : ∀ R ∈ descendantsAtScale Q n, X (cubeSet R) =ᵐ[P] Y (cubeSet R)) : restrictionCenteredDescendantAverageOnCube P Q n X =ᵐ[P] restrictionCenteredDescendantAverageOnCube P Q n Y

A.e.-equal descendant observables, with a.e.-equal origin representatives for the centering constant, have the same centered descendant average on a fixed parent cube.

theorem HCPolySupport.Book.Ch04.centeredDescendantAverage_eq_descendantAverage_sub_originMean {d : ℕ} {P : RestrictionCoeffLaw d} {Q : TriadicCube d} {n : ℤ} (hnQ : n ≤ Q.scale) (X : Set (Vec d) → RegCoeffField d → ℝ) : restrictionCenteredDescendantAverageOnCube P Q n X = fun (a : RegCoeffField d) => restrictionDescendantAverageOnCube Q n X a - ∫ (b : RegCoeffField d), X (cubeSet (originCube d n)) b ∂P

The centered descendant average on an arbitrary parent cube is the uncentered descendant average minus the origin-cube centering constant.

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.restrictionResponseJCubeObservable {d : ℕ} (p q : Vec d) : Set (Vec d) → RegCoeffField d → ℝ

The response observable U ↦ J(U,p,q;·) used in the special partition average corollary.

Equations

• HCPolySupport.Book.Ch04.restrictionResponseJCubeObservable p q U a = HCPolySupport.ResponseJ U p q a.toFun

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.restrictionCenteredResponseJOriginObservable {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) (p q : Vec d) : RegCoeffField d → ℝ

The response observable on the origin cube, centered by its expectation.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.restrictionResponseJDescendantAverage {d : ℕ} (n m : ℤ) (p q : Vec d) : RegCoeffField d → ℝ

The uncentered partition average of the response functional over scale-n descendants of the origin cube at scale m.

Equations

• HCPolySupport.Book.Ch04.restrictionResponseJDescendantAverage n m p q = HCPolySupport.Book.Ch04.restrictionDescendantAverage n m (HCPolySupport.Book.Ch04.restrictionResponseJCubeObservable p q)

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.restrictionCenteredResponseJDescendantAverage {d : ℕ} (P : RestrictionCoeffLaw d) (n m : ℤ) (p q : Vec d) : RegCoeffField d → ℝ

The centered partition average of the response functional over scale-n descendants of the origin cube at scale m.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch04.rosenthalDescendantsAtScaleLpConst (d : ℕ) (k : ℤ) (p : ℕ) : ℝ

Exact Chapter 4 color-count constant multiplying the genuinely L^p Rosenthal term in the partition-average fluctuation bound.

Equations

• HCPolySupport.Book.Ch04.rosenthalDescendantsAtScaleLpConst d k p = 2 * ↑p * ↑(HCPolySupport.scaleColorPeriod k ^ d) ^ (1 - 1 / ↑p)

noncomputable def HCPolySupport.Book.Ch04.rosenthalDescendantsAtScaleSqrtConst (d : ℕ) (k : ℤ) (p : ℕ) : ℝ

Exact Chapter 4 color-count constant multiplying the square-function Rosenthal term in the partition-average fluctuation bound.

Equations

• HCPolySupport.Book.Ch04.rosenthalDescendantsAtScaleSqrtConst d k p = 4 * HCPolySupport.Book.Ch04.rosenthalBennettIntegralConst * (√↑p * √↑(HCPolySupport.scaleColorPeriod k ^ d))