Coarse-graining support: Support.Book.Ch04.Theorems.AnnealedSubadditivity.LawCarrierAEBounds

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

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.restrictionResponseJObservableCubeSet_le_descendantsAverage_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {n m : ℤ} (hnm : n ≤ m) (p q : Vec d) : restrictionResponseJObservableCubeSet (originCube d m) p q ≤ᵐ[P] fun (a : RegCoeffField d) => descendantsAverage (originCube d m) (m - n).toNat fun (R : TriadicCube d) => restrictionResponseJObservableCubeSet R p q a

The deterministic descendant-average comparison for scalar response observables holds almost surely under a law carrier.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.coarseBlockMatrix_le_descendantsAverageBlockMat_cubeSet_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) : ∀ᵐ (a : RegCoeffField d) ∂P, BlockMatLoewnerLE (coarseBlockMatrix (cubeSet Q) a.toFun) (descendantsAverageBlockMat Q (Q.scale - k).toNat fun (R : TriadicCube d) => coarseBlockMatrix (cubeSet R) a.toFun)

The deterministic descendant-average comparison for coarse block matrices on an arbitrary triadic cube holds almost surely under a law carrier.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.coarseBlockMatrix_le_descendantsAverageBlockMat_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {n m : ℤ} (hnm : n ≤ m) : ∀ᵐ (a : RegCoeffField d) ∂P, BlockMatLoewnerLE (coarseBlockMatrix (cubeSet (originCube d m)) a.toFun) (descendantsAverageBlockMat (originCube d m) (m - n).toNat fun (R : TriadicCube d) => coarseBlockMatrix (cubeSet R) a.toFun)

The deterministic descendant-average comparison for coarse block matrices holds almost surely under a law carrier.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.coarseMatrix_upperLeft_apply_excessPart_le_abs_centeredDescendantMean_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (i : Fin d) : (fun (a : RegCoeffField d) => max ((coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft i i - ∫ (b : RegCoeffField d), (coarseBlockMatrix (cubeSet (originCube d k)) b.toFun).upperLeft i i ∂P) 0) ≤ᵐ[P] fun (a : RegCoeffField d) => |restrictionCenteredDescendantAverageOnCube P Q k (fun (U : Set (Vec d)) (a : RegCoeffField d) => (coarseBlockMatrix U a.toFun).upperLeft i i) a|

Diagonal upper-left block positive excess is controlled by the centered descendant average of the corresponding entry observable.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.coarseMatrix_upperLeft_normExcess_le_sum_abs_centeredDescendantMean_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (center : Mat d) (hcenter : ∀ (i j : Fin d), center i j = ∫ (b : RegCoeffField d), (coarseBlockMatrix (cubeSet (originCube d k)) b.toFun).upperLeft i j ∂P) : (fun (a : RegCoeffField d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft - Ch02.matrixNorm center) 0) ≤ᵐ[P] fun (a : RegCoeffField d) => ∑ i : Fin d, ∑ j : Fin d, |restrictionCenteredDescendantAverageOnCube P Q k (fun (U : Set (Vec d)) (a : RegCoeffField d) => (coarseBlockMatrix U a.toFun).upperLeft i j) a|

Operator-norm upper-left positive excess is controlled by the entrywise centered descendant-average fluctuations. The norm here is Ch02.matrixNorm, i.e. the matrix operator norm.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.coarseMatrix_upperLeft_normExcess_finiteSup_le_sum_finiteSup_centeredMean_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {parents : Finset (TriadicCube d)} (hparents : parents.Nonempty) {k : ℤ} (hparent_scale : ∀ Q ∈ parents, k ≤ Q.scale) (center : Mat d) (hcenter : ∀ (i j : Fin d), center i j = ∫ (b : RegCoeffField d), (coarseBlockMatrix (cubeSet (originCube d k)) b.toFun).upperLeft i j ∂P) : (fun (a : RegCoeffField d) => parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft - Ch02.matrixNorm center) 0) ≤ᵐ[P] fun (a : RegCoeffField d) => ∑ i : Fin d, ∑ j : Fin d, parents.sup' hparents fun (Q : TriadicCube d) => |restrictionCenteredDescendantAverageOnCube P Q k (fun (U : Set (Vec d)) (a : RegCoeffField d) => (coarseBlockMatrix U a.toFun).upperLeft i j) a|

Finite-parent version of the upper-left operator-norm positive-excess domination. This is the clean raw deterministic input for the Ch4 large-scale fluctuation theorem: no representative observable is exposed.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.coarseMatrix_upperLeft_normExcess_le_sum_abs_centeredDescendantMean_rep_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (center : Mat d) (hcenter : ∀ (i j : Fin d), center i j = ∫ (b : RegCoeffField d), (coarseBlockMatrix (cubeSet (originCube d k)) b.toFun).upperLeft i j ∂P) (Y : Fin d → Fin d → Set (Vec d) → RegCoeffField d → ℝ) (hOrigin : ∀ (i j : Fin d), (fun (a : RegCoeffField d) => (coarseBlockMatrix (cubeSet (originCube d k)) a.toFun).upperLeft i j) =ᵐ[P] Y i j (cubeSet (originCube d k))) (hDesc : ∀ (i j : Fin d), ∀ R ∈ descendantsAtScale Q k, (fun (a : RegCoeffField d) => (coarseBlockMatrix (cubeSet R) a.toFun).upperLeft i j) =ᵐ[P] Y i j (cubeSet R)) : (fun (a : RegCoeffField d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft - Ch02.matrixNorm center) 0) ≤ᵐ[P] fun (a : RegCoeffField d) => ∑ i : Fin d, ∑ j : Fin d, |restrictionCenteredDescendantAverageOnCube P Q k (Y i j) a|

Representative version of coarseMatrix_upperLeft_normExcess_le_sum_abs_centeredDescendantMean_ae. Each entry may be replaced by an a.e.-equal local/measurable representative before applying the probabilistic partition-average theorem.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.coarseMatrix_upperLeft_apply_excessPart_le_abs_centeredDescendantMean_rep_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (i : Fin d) (Y : Set (Vec d) → RegCoeffField d → ℝ) (hOrigin : (fun (a : RegCoeffField d) => (coarseBlockMatrix (cubeSet (originCube d k)) a.toFun).upperLeft i i) =ᵐ[P] Y (cubeSet (originCube d k))) (hDesc : ∀ R ∈ descendantsAtScale Q k, (fun (a : RegCoeffField d) => (coarseBlockMatrix (cubeSet R) a.toFun).upperLeft i i) =ᵐ[P] Y (cubeSet R)) : (fun (a : RegCoeffField d) => max ((coarseBlockMatrix (cubeSet Q) a.toFun).upperLeft i i - ∫ (b : RegCoeffField d), (coarseBlockMatrix (cubeSet (originCube d k)) b.toFun).upperLeft i i ∂P) 0) ≤ᵐ[P] fun (a : RegCoeffField d) => |restrictionCenteredDescendantAverageOnCube P Q k Y a|

Same upper-left diagonal positive-excess control, after replacing the raw coarse-block entry by an a.e.-equal representative. This is the form consumed by local/measurable representative arguments.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.coarseMatrix_lowerRight_apply_excessPart_le_abs_centeredDescendantMean_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (i : Fin d) : (fun (a : RegCoeffField d) => max ((coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight i i - ∫ (b : RegCoeffField d), (coarseBlockMatrix (cubeSet (originCube d k)) b.toFun).lowerRight i i ∂P) 0) ≤ᵐ[P] fun (a : RegCoeffField d) => |restrictionCenteredDescendantAverageOnCube P Q k (fun (U : Set (Vec d)) (a : RegCoeffField d) => (coarseBlockMatrix U a.toFun).lowerRight i i) a|

Diagonal lower-right block positive excess is controlled by the centered descendant average of the corresponding entry observable.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.coarseMatrix_lowerRight_normExcess_le_sum_abs_centeredDescendantMean_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (center : Mat d) (hcenter : ∀ (i j : Fin d), center i j = ∫ (b : RegCoeffField d), (coarseBlockMatrix (cubeSet (originCube d k)) b.toFun).lowerRight i j ∂P) : (fun (a : RegCoeffField d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight - Ch02.matrixNorm center) 0) ≤ᵐ[P] fun (a : RegCoeffField d) => ∑ i : Fin d, ∑ j : Fin d, |restrictionCenteredDescendantAverageOnCube P Q k (fun (U : Set (Vec d)) (a : RegCoeffField d) => (coarseBlockMatrix U a.toFun).lowerRight i j) a|

Operator-norm lower-right positive excess is controlled by the entrywise centered descendant-average fluctuations. The norm here is Ch02.matrixNorm, i.e. the matrix operator norm.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.coarseMatrix_lowerRight_normExcess_finiteSup_le_sum_finiteSup_centeredMean_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {parents : Finset (TriadicCube d)} (hparents : parents.Nonempty) {k : ℤ} (hparent_scale : ∀ Q ∈ parents, k ≤ Q.scale) (center : Mat d) (hcenter : ∀ (i j : Fin d), center i j = ∫ (b : RegCoeffField d), (coarseBlockMatrix (cubeSet (originCube d k)) b.toFun).lowerRight i j ∂P) : (fun (a : RegCoeffField d) => parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight - Ch02.matrixNorm center) 0) ≤ᵐ[P] fun (a : RegCoeffField d) => ∑ i : Fin d, ∑ j : Fin d, parents.sup' hparents fun (Q : TriadicCube d) => |restrictionCenteredDescendantAverageOnCube P Q k (fun (U : Set (Vec d)) (a : RegCoeffField d) => (coarseBlockMatrix U a.toFun).lowerRight i j) a|

Finite-parent version of the lower-right operator-norm positive-excess domination. This is the clean raw deterministic input for the Ch4 large-scale fluctuation theorem: no representative observable is exposed.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.coarseMatrix_lowerRight_normExcess_le_sum_abs_centeredDescendantMean_rep_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (center : Mat d) (hcenter : ∀ (i j : Fin d), center i j = ∫ (b : RegCoeffField d), (coarseBlockMatrix (cubeSet (originCube d k)) b.toFun).lowerRight i j ∂P) (Y : Fin d → Fin d → Set (Vec d) → RegCoeffField d → ℝ) (hOrigin : ∀ (i j : Fin d), (fun (a : RegCoeffField d) => (coarseBlockMatrix (cubeSet (originCube d k)) a.toFun).lowerRight i j) =ᵐ[P] Y i j (cubeSet (originCube d k))) (hDesc : ∀ (i j : Fin d), ∀ R ∈ descendantsAtScale Q k, (fun (a : RegCoeffField d) => (coarseBlockMatrix (cubeSet R) a.toFun).lowerRight i j) =ᵐ[P] Y i j (cubeSet R)) : (fun (a : RegCoeffField d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight - Ch02.matrixNorm center) 0) ≤ᵐ[P] fun (a : RegCoeffField d) => ∑ i : Fin d, ∑ j : Fin d, |restrictionCenteredDescendantAverageOnCube P Q k (Y i j) a|

Representative version of coarseMatrix_lowerRight_normExcess_le_sum_abs_centeredDescendantMean_ae. Each entry may be replaced by an a.e.-equal local/measurable representative before applying the probabilistic partition-average theorem.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.coarseMatrix_lowerRight_apply_excessPart_le_abs_centeredDescendantMean_rep_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (i : Fin d) (Y : Set (Vec d) → RegCoeffField d → ℝ) (hOrigin : (fun (a : RegCoeffField d) => (coarseBlockMatrix (cubeSet (originCube d k)) a.toFun).lowerRight i i) =ᵐ[P] Y (cubeSet (originCube d k))) (hDesc : ∀ R ∈ descendantsAtScale Q k, (fun (a : RegCoeffField d) => (coarseBlockMatrix (cubeSet R) a.toFun).lowerRight i i) =ᵐ[P] Y (cubeSet R)) : (fun (a : RegCoeffField d) => max ((coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight i i - ∫ (b : RegCoeffField d), (coarseBlockMatrix (cubeSet (originCube d k)) b.toFun).lowerRight i i ∂P) 0) ≤ᵐ[P] fun (a : RegCoeffField d) => |restrictionCenteredDescendantAverageOnCube P Q k Y a|

Same lower-right diagonal positive-excess control, after replacing the raw coarse-block entry by an a.e.-equal representative.