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

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

theorem HCPolySupport.Book.Ch04.IsAEEllipticFieldOn.adjointCoeffField {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (h : IsAEEllipticFieldOn lam Lam U a) : IsAEEllipticFieldOn lam Lam U (HCPolySupport.adjointCoeffField a)

theorem HCPolySupport.Book.Ch04.adjointReg_toFun {d : ℕ} (a : RegCoeffField d) : (adjointReg a).toFun = adjointCoeffField a.toFun

The underlying field of the carrier adjoint is the raw field adjoint.

theorem HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField.adjointReg {d : ℕ} {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) : AELocallyUniformlyEllipticField (HCPolySupport.adjointReg a)

Carrier a.e.-ellipticity transports under the carrier adjoint endomorphism: the transpose preserves the local uniform elliptic bounds.

theorem HCPolySupport.Book.Ch04.exists_restrictionLocalRandomVariable_ae_eq_coarseUpperRightEntry {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (i j : Fin d) : ∃ (Y : RegCoeffField d → ℝ), IsRestrictionLocalRandomVariable (cubeSet Q) ⋯ Y ∧ (fun (a : RegCoeffField d) => (coarseBlockMatrix (cubeSet Q) a.toFun).upperRight i j) =ᵐ[P] Y

theorem HCPolySupport.Book.Ch04.exists_restrictionLocalRandomVariable_ae_eq_coarseLowerLeftEntry {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (i j : Fin d) : ∃ (Y : RegCoeffField d → ℝ), IsRestrictionLocalRandomVariable (cubeSet Q) ⋯ Y ∧ (fun (a : RegCoeffField d) => (coarseBlockMatrix (cubeSet Q) a.toFun).lowerLeft i j) =ᵐ[P] Y

theorem HCPolySupport.Book.Ch04.exists_isRestrictionLocalRandomVariable_ae_eq_coarseFullBlockMatrix_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) : ∃ (Y : RegCoeffField d → FullBlockMat d), IsRestrictionLocalRandomVariable (cubeSet Q) ⋯ Y ∧ (fun (a : RegCoeffField d) => toFullBlockMat (coarseBlockMatrix (cubeSet Q) a.toFun)) =ᵐ[P] Y

noncomputable def HCPolySupport.Book.Ch04.blockJObservableCubeSetBlockVec {d : ℕ} (Q : TriadicCube d) (P Qv : BlockVec d) : RegCoeffField d → ℝ

The cube block-response observable with its four vector inputs packaged as block vectors.

Equations

• HCPolySupport.Book.Ch04.blockJObservableCubeSetBlockVec Q P Qv = HCPolySupport.Book.Ch04.blockJObservableCubeSet Q P.1 Qv.2 P.2 Qv.1

theorem HCPolySupport.Book.Ch04.blockJObservableCubeSetBlockVec_nonneg {d : ℕ} (Q : TriadicCube d) (P Qv : BlockVec d) (a : RegCoeffField d) : 0 ≤ blockJObservableCubeSetBlockVec Q P Qv a

theorem HCPolySupport.Book.Ch04.blockJObservable_le_descendantAverage_of_uniformEllipticity {d : ℕ} [NeZero d] {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (P Qv : BlockVec d) : blockJObservableCubeSetBlockVec Q P Qv a ≤ descendantsAverage Q (Q.scale - k).toNat fun (R : TriadicCube d) => blockJObservableCubeSetBlockVec R P Qv a

theorem HCPolySupport.Book.Ch04.doubledResponseJ_eq_blockJObservableCubeSetBlockVec_of_aelocallyUniformlyEllipticField {d : ℕ} [NeZero d] {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (P Qv : BlockVec d) : Ch02.doubledResponseJ (Ch02.cubeDomain Q) ((triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) P Qv = blockJObservableCubeSetBlockVec Q P Qv a

def HCPolySupport.Book.Ch04.fullBlockReflect {d : ℕ} (M : FullBlockMat d) : FullBlockMat d

Block reflection transported to the full-matrix representation used for response quadratics.

Equations

• HCPolySupport.Book.Ch04.fullBlockReflect M = HCPolySupport.toFullBlockMat (HCPolySupport.blockReflect (HCPolySupport.ofFullBlockMat M))

def HCPolySupport.Book.Ch04.fullBlockQuadraticCh04 {d : ℕ} (M : FullBlockMat d) (x : FullBlockVec d) : ℝ

The quadratic form x · (M x) used to express block responses in full-matrix coordinates.

Equations

• HCPolySupport.Book.Ch04.fullBlockQuadraticCh04 M x = x ⬝ᵥ Matrix.mulVec M x

noncomputable def HCPolySupport.Book.Ch04.blockJQuadraticFullBlockMat {d : ℕ} (M : FullBlockMat d) (P Qv : BlockVec d) : ℝ

The block-response quadratic: half the forms for M and its reflection, minus the pairing of the two block vectors.

Equations

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

@[simp]

theorem HCPolySupport.Book.Ch04.fullBlockReflect_toFullBlockMat {d : ℕ} (A : BlockMat d) : fullBlockReflect (toFullBlockMat A) = toFullBlockMat (blockReflect A)

theorem HCPolySupport.Book.Ch04.fullBlockQuadraticCh04_toFullBlockMat {d : ℕ} (A : BlockMat d) (P : BlockVec d) : fullBlockQuadraticCh04 (toFullBlockMat A) (toFullBlockVec P) = blockVecDot P (blockMatVecMul A P)

theorem HCPolySupport.Book.Ch04.blockJObservable_eq_blockJQuadraticForm_of_uniformEllipticity {d : ℕ} [NeZero d] {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (P Qv : BlockVec d) : blockJObservableCubeSetBlockVec Q P Qv a = blockJQuadraticFullBlockMat (toFullBlockMat (coarseBlockMatrix (cubeSet Q) a.toFun)) P Qv

theorem HCPolySupport.Book.Ch04.blockJObservableCubeSetBlockVec_ae_eq_blockJQuadraticFullBlockMat {d : ℕ} [NeZero d] {Pμ : RestrictionCoeffLaw d} (hPμ : RestrictionLawCarrier Pμ) (Q : TriadicCube d) (P Qv : BlockVec d) : blockJObservableCubeSetBlockVec Q P Qv =ᵐ[Pμ] fun (a : RegCoeffField d) => blockJQuadraticFullBlockMat (toFullBlockMat (coarseBlockMatrix (cubeSet Q) a.toFun)) P Qv

theorem HCPolySupport.Book.Ch04.exists_isRestrictionLocalRandomVariable_ae_eq_blockJObservableCubeSetBlockVec {d : ℕ} [NeZero d] {Pμ : RestrictionCoeffLaw d} (hPμ : RestrictionLawCarrier Pμ) (Q : TriadicCube d) (P Qv : BlockVec d) : ∃ (Y : RegCoeffField d → ℝ), IsRestrictionLocalRandomVariable (cubeSet Q) ⋯ Y ∧ blockJObservableCubeSetBlockVec Q P Qv =ᵐ[Pμ] Y

noncomputable def HCPolySupport.Book.Ch04.blockJSetObservableBlockVec {d : ℕ} (P Qv : BlockVec d) : Set (Vec d) → CoeffField d → ℝ

The setwise half-sum of a response and its adjoint response, with block-vector inputs.

Equations

• HCPolySupport.Book.Ch04.blockJSetObservableBlockVec P Qv U = HCPolySupport.Book.Ch04.blockJHalfResponseAdjointSumSet U P.1 Qv.2 P.2 Qv.1

@[simp]

theorem HCPolySupport.Book.Ch04.blockJSetObservableBlockVec_cubeSet {d : ℕ} (Q : TriadicCube d) (P Qv : BlockVec d) (a : RegCoeffField d) : blockJSetObservableBlockVec P Qv (cubeSet Q) a.toFun = blockJObservableCubeSetBlockVec Q P Qv a

The raw set-observable, precomposed with the honest sample on a triadic cube, is the carrier block-response observable.

theorem HCPolySupport.Book.Ch04.blockJSetObservableBlockVec_translation_covariant {d : ℕ} (P Qv : BlockVec d) : IsTranslationCovariant (blockJSetObservableBlockVec P Qv)

theorem HCPolySupport.Book.Ch04.blockJSetObservableBlockVec_restrictionTranslationCovariant {d : ℕ} (P Qv : BlockVec d) : IsRestrictionTranslationCovariant fun (U : Set (Vec d)) (a : RegCoeffField d) => blockJSetObservableBlockVec P Qv U a.toFun

Restriction translation covariance of the raw set-observable precomposed with the honest sample.

theorem HCPolySupport.Book.Ch04.exists_isRestrictionLocalRandomVariable_ae_eq_blockJSetObservableBlockVec_cubeSet {d : ℕ} [NeZero d] {Pμ : RestrictionCoeffLaw d} (hPμ : RestrictionLawCarrier Pμ) (Q : TriadicCube d) (P Qv : BlockVec d) : ∃ (Y : RegCoeffField d → ℝ), IsRestrictionLocalRandomVariable (cubeSet Q) ⋯ Y ∧ (fun (a : RegCoeffField d) => blockJSetObservableBlockVec P Qv (cubeSet Q) a.toFun) =ᵐ[Pμ] Y

theorem HCPolySupport.Book.Ch04.aemeasurable_blockJSetObservableBlockVec_cubeSet {d : ℕ} [NeZero d] {Pμ : RestrictionCoeffLaw d} (hPμ : RestrictionLawCarrier Pμ) (Q : TriadicCube d) (P Qv : BlockVec d) : AEMeasurable (fun (a : RegCoeffField d) => blockJSetObservableBlockVec P Qv (cubeSet Q) a.toFun) Pμ

theorem HCPolySupport.Book.Ch04.isBigO_gammaSigma_blockJObservableCubeSetBlockVec_originCube_of_scaleZero {d : ℕ} [NeZero d] {Pμ : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure Pμ] {σ θ : ℝ} (hPμ : RestrictionLawCarrier Pμ) (hstat : RestrictionStationaryLaw Pμ) (hσ : 0 < σ) (hθ : 0 < θ) (P Qv : BlockVec d) (h0 : IsBigO Pμ (gammaSigma σ) (blockJObservableCubeSetBlockVec (originCube d 0) P Qv) θ) {n : ℤ} (hn : 0 ≤ n) : IsBigO Pμ (gammaSigma σ) (blockJObservableCubeSetBlockVec (originCube d n) P Qv) (gammaTriangleConst σ * θ)

theorem HCPolySupport.Book.Ch04.isBigO_gammaSigma_centeredOrigin_blockJSetObservableBlockVec_of_scaleZero {d : ℕ} [NeZero d] {Pμ : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure Pμ] {σ θ : ℝ} (hPμ : RestrictionLawCarrier Pμ) (hstat : RestrictionStationaryLaw Pμ) (hσ : 0 < σ) (hθ : 0 < θ) (P Qv : BlockVec d) (h0 : IsBigO Pμ (gammaSigma σ) (blockJObservableCubeSetBlockVec (originCube d 0) P Qv) θ) {n : ℤ} (hn : 0 ≤ n) : IsBigO Pμ (gammaSigma σ) (restrictionCenteredOriginObservable Pμ n fun (U : Set (Vec d)) (a : RegCoeffField d) => blockJSetObservableBlockVec P Qv U a.toFun) (gammaTriangleConst σ * (gammaTriangleConst σ * θ + gammaMomentConst σ * (gammaTriangleConst σ * θ)))

theorem HCPolySupport.Book.Ch04.isBigOWith_gammaSigma_blockJObservableCubeSetBlockVec_originCube_sub_integral {d : ℕ} [NeZero d] {Pμ : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure Pμ] {σ θ : ℝ} (hPμ : RestrictionLawCarrier Pμ) (hstat : RestrictionStationaryLaw Pμ) (hdep : RestrictionUnitRangeDependentLaw Pμ) (hσ₀ : 0 < σ) (hσ₂ : σ ≤ 2) (hθ : 0 < θ) (P Qv : BlockVec d) (h0 : IsBigO Pμ (gammaSigma σ) (blockJObservableCubeSetBlockVec (originCube d 0) P Qv) θ) {n m : ℤ} (hn : 0 ≤ n) (hnm : n < m) : IsBigOWith Pμ (gammaSigma σ) (fun (a : RegCoeffField d) => blockJObservableCubeSetBlockVec (originCube d m) P Qv a - ∫ (b : RegCoeffField d), blockJObservableCubeSetBlockVec (originCube d n) P Qv b ∂Pμ) (gammaSigmaDescendantsAtScaleConst d n σ * (√↑(descendantsAtScale (originCube d m) n).card / ↑(descendantsAtScale (originCube d m) n).card) * (gammaTriangleConst σ * (gammaTriangleConst σ * θ + gammaMomentConst σ * (gammaTriangleConst σ * θ))))

noncomputable def HCPolySupport.Book.Ch04.blockJConcentrationConst (d : ℕ) (σ : ℝ) : ℝ

The dimension- and moment-dependent prefactor in the block-response concentration bound.

Equations

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

theorem HCPolySupport.Book.Ch04.blockJConcentrationConst_pos {d : ℕ} {σ : ℝ} (hσ : 0 < σ) : 0 < blockJConcentrationConst d σ

theorem HCPolySupport.Book.Ch04.concentration_of_blockJObservableCubeSetBlockVec {d : ℕ} [NeZero d] {σ : ℝ} (hσ₀ : 0 < σ) (hσ₂ : σ ≤ 2) : ∃ (C : ℝ), 0 < C ∧ ∀ {θ : ℝ}, 0 < θ → ∀ {Pμ : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure Pμ], RestrictionLawCarrier Pμ → RestrictionStationaryLaw Pμ → RestrictionUnitRangeDependentLaw Pμ → ∀ (P Qv : BlockVec d), IsBigO Pμ (gammaSigma σ) (blockJObservableCubeSetBlockVec (originCube d 0) P Qv) θ → ∀ {n m : ℤ}, 0 ≤ n → n < m → IsBigOWith Pμ (gammaSigma σ) (fun (a : RegCoeffField d) => blockJObservableCubeSetBlockVec (originCube d m) P Qv a - ∫ (b : RegCoeffField d), blockJObservableCubeSetBlockVec (originCube d n) P Qv b ∂Pμ) (C * 3 ^ (-↑d / 2 * ↑(m - n).toNat) * θ)

Lemma l.concentration.of.J, in the block-vector form used by the Lean development. The manuscript's normalized pair (B^{-1/2}e, B^{1/2}e) is obtained by specializing P and Qv.

The constant is chosen before θ, the law, the vectors, and the scales.