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

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

Scalarization definitions

Scalar-matrix helper lemmas and the internal scalarization route used to prove the public Chapter 4 scalar selectors.

structure HCPolySupport.Book.Ch04.Internal.AnnealedScalarizationTheory {d : ℕ} (P : RestrictionCoeffLaw d) : Prop

Internal route package for scalarization of the annealed coarse-grained matrices on origin cubes. Public callers should use the direct RestrictionLawCarrier.*AtScale scalar selectors instead.

• scalarized (n : ℤ) : HasAnnealedScalarizationAtScale P n

noncomputable def HCPolySupport.Book.Ch04.Internal.AnnealedScalarizationTheory.witness {d : ℕ} {P : RestrictionCoeffLaw d} (h : AnnealedScalarizationTheory P) (n : ℤ) : AnnealedScalarizationWitness P n

The chosen scalarization witness at scale n.

Equations

• h.witness n = Classical.choice ⋯

noncomputable def HCPolySupport.Book.Ch04.Internal.AnnealedScalarizationTheory.barSigma {d : ℕ} {P : RestrictionCoeffLaw d} (h : AnnealedScalarizationTheory P) (n : ℤ) : ℝ

The scalar \bar\sigma_n.

Equations

• h.barSigma n = (h.witness n).sigma

noncomputable def HCPolySupport.Book.Ch04.Internal.AnnealedScalarizationTheory.barSigmaStar {d : ℕ} {P : RestrictionCoeffLaw d} (h : AnnealedScalarizationTheory P) (n : ℤ) : ℝ

The scalar \bar\sigma_{*,n}.

Equations

• h.barSigmaStar n = (h.witness n).sigmaStar

theorem HCPolySupport.Book.Ch04.Internal.AnnealedScalarizationTheory.annealedSigma_eq {d : ℕ} {P : RestrictionCoeffLaw d} (h : AnnealedScalarizationTheory P) (n : ℤ) : annealedSigmaAtScale P n = h.barSigma n • 1

theorem HCPolySupport.Book.Ch04.Internal.AnnealedScalarizationTheory.annealedSigmaStar_eq {d : ℕ} {P : RestrictionCoeffLaw d} (h : AnnealedScalarizationTheory P) (n : ℤ) : annealedSigmaStarAtScale P n = h.barSigmaStar n • 1

theorem HCPolySupport.Book.Ch04.Internal.AnnealedScalarizationTheory.annealedKappa_eq_zero {d : ℕ} {P : RestrictionCoeffLaw d} (h : AnnealedScalarizationTheory P) (n : ℤ) : annealedKappaAtScale P n = 0

noncomputable def HCPolySupport.Book.Ch04.Internal.AnnealedScalarizationTheory.contrast {d : ℕ} {P : RestrictionCoeffLaw d} (h : AnnealedScalarizationTheory P) (n : ℤ) : ℝ

The scalar contrast ratio used downstream.

Equations

• h.contrast n = h.barSigma n * (h.barSigmaStar n)⁻¹

theorem HCPolySupport.Book.Ch04.scalar_le_of_matLoewnerLE_smul_one {d : ℕ} [NeZero d] {a b : ℝ} (h : MatLoewnerLE (a • 1) (b • 1)) : a ≤ b

A Löwner comparison between scalar matrices is the corresponding scalar comparison.

theorem HCPolySupport.Book.Ch04.matLoewnerLE_smul_one_of_scalar_le {d : ℕ} {a b : ℝ} (h : a ≤ b) : MatLoewnerLE (a • 1) (b • 1)

Scalar comparisons lift to Löwner comparisons between scalar identity matrices.

theorem HCPolySupport.Book.Ch04.scalar_eq_of_smul_one_eq_smul_one {d : ℕ} [NeZero d] {a b : ℝ} (h : a • 1 = b • 1) : a = b

Scalar coefficients of scalar identity matrices are unique.

theorem HCPolySupport.Book.Ch04.integral_pos_of_integrable_pos_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {f : α → ℝ} (hfint : MeasureTheory.Integrable f μ) (hfpos : ∀ᵐ (x : α) ∂μ, 0 < f x) : 0 < ∫ (x : α), f x ∂μ

A strictly positive a.e. integrable real function has strictly positive expectation under a probability measure.

theorem HCPolySupport.Book.Ch04.matrix_posDef_diag_pos {d : ℕ} {A : Mat d} (hA : Matrix.PosDef A) (i : Fin d) : 0 < A i i

theorem HCPolySupport.Book.Ch04.scalar_coefficient_pos_of_smul_one_eq_integral_posDef {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {d : ℕ} [NeZero d] {F : α → Mat d} {c : ℝ} (hFint : MeasureTheory.Integrable F μ) (hPos : ∀ᵐ (x : α) ∂μ, Matrix.PosDef (F x)) (hScalar : ∫ (x : α), F x ∂μ = c • 1) : 0 < c

If the integral of an a.e. positive-definite matrix field is a scalar multiple of the identity, then the scalar coefficient is positive.

@[reducible, inline]

abbrev HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData {d : ℕ} [NeZero d] (P : RestrictionCoeffLaw d) (n : ℤ) : Prop

Internal primitive scalarization data for the inverse-star and upper-left annealed blocks. Public callers should use direct structural-law endpoints.

Equations

• HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData P n = HCPolySupport.Book.Ch04.Internal.AnnealedScalarizationPrimitiveData P n

noncomputable def HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData.barSigmaStarInv {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} (h : AnnealedPrimitiveScalarizationData P n) : ℝ

The scalar coefficient of the annealed inverse-star block.

Equations

• h.barSigmaStarInv = Classical.choose ⋯

noncomputable def HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData.barB {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} (h : AnnealedPrimitiveScalarizationData P n) : ℝ

The scalar coefficient of the annealed upper-left block.

Equations

• h.barB = Classical.choose ⋯

noncomputable def HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData.contrast {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} (h : AnnealedPrimitiveScalarizationData P n) : ℝ

The primitive scalar contrast used by downstream estimates.

Equations

• h.contrast = h.barB * h.barSigmaStarInv

theorem HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData.sigmaStarInv_eq {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} (h : AnnealedPrimitiveScalarizationData P n) : annealedSigmaStarInvAtScale P n = h.barSigmaStarInv • 1

theorem HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData.b_eq {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} (h : AnnealedPrimitiveScalarizationData P n) : annealedBAtScale P n = h.barB • 1

theorem HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData.sigma_eq {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} (h : AnnealedPrimitiveScalarizationData P n) : annealedSigmaAtScale P n = h.barB • 1

theorem HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData.kappa_eq_zero {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} (h : AnnealedPrimitiveScalarizationData P n) : annealedKappaAtScale P n = 0

theorem HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData.barSigma_eq_barB {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} (hScal : AnnealedScalarizationTheory P) (hPrim : AnnealedPrimitiveScalarizationData P n) : hScal.barSigma n = hPrim.barB

theorem HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData.barSigmaStar_eq_inv_barSigmaStarInv {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} (hScal : AnnealedScalarizationTheory P) (hPrim : AnnealedPrimitiveScalarizationData P n) : hScal.barSigmaStar n = hPrim.barSigmaStarInv⁻¹

theorem HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData.scalar_contrast_eq {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} (hScal : AnnealedScalarizationTheory P) (hPrim : AnnealedPrimitiveScalarizationData P n) : hScal.contrast n = hPrim.contrast

theorem HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData.barSigmaStarInv_le_of_matLoewnerLE {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {m n : ℤ} (hm : AnnealedPrimitiveScalarizationData P m) (hn : AnnealedPrimitiveScalarizationData P n) (hLE : MatLoewnerLE (annealedSigmaStarInvAtScale P m) (annealedSigmaStarInvAtScale P n)) : hm.barSigmaStarInv ≤ hn.barSigmaStarInv

theorem HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData.barB_le_of_matLoewnerLE {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {m n : ℤ} (hm : AnnealedPrimitiveScalarizationData P m) (hn : AnnealedPrimitiveScalarizationData P n) (hLE : MatLoewnerLE (annealedBAtScale P m) (annealedBAtScale P n)) : hm.barB ≤ hn.barB

theorem HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData.contrast_le_of_component_le {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {m n : ℤ} (hm : AnnealedPrimitiveScalarizationData P m) (hn : AnnealedPrimitiveScalarizationData P n) (hB_le : hm.barB ≤ hn.barB) (hStar_le : hm.barSigmaStarInv ≤ hn.barSigmaStarInv) (hStar_m_nonneg : 0 ≤ hm.barSigmaStarInv) (hB_n_nonneg : 0 ≤ hn.barB) : hm.contrast ≤ hn.contrast

theorem HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData.barSigmaStar_le_of_barSigmaStarInv_le {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n m : ℤ} (hScal : AnnealedScalarizationTheory P) (hm : AnnealedPrimitiveScalarizationData P m) (hn : AnnealedPrimitiveScalarizationData P n) (hStar_le : hm.barSigmaStarInv ≤ hn.barSigmaStarInv) (hStar_m_pos : 0 < hm.barSigmaStarInv) : hScal.barSigmaStar n ≤ hScal.barSigmaStar m

theorem HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData.barSigmaStar_le_barSigma_of_one_le_contrast {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} (hScal : AnnealedScalarizationTheory P) (hPrim : AnnealedPrimitiveScalarizationData P n) (hContrast : 1 ≤ hPrim.contrast) (hStar_pos : 0 < hPrim.barSigmaStarInv) : hScal.barSigmaStar n ≤ hScal.barSigma n

theorem HCPolySupport.Book.Ch04.Internal.AnnealedPrimitiveScalarizationData.barSigma_le_of_barB_le {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n m : ℤ} (hScal : AnnealedScalarizationTheory P) (hm : AnnealedPrimitiveScalarizationData P m) (hn : AnnealedPrimitiveScalarizationData P n) (hB_le : hm.barB ≤ hn.barB) : hScal.barSigma m ≤ hScal.barSigma n

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.Internal.barBAtScaleOfPrimitive {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} (h : AnnealedPrimitiveScalarizationData P n) : ℝ

Internal scalar coefficient of the primitive upper-left block.

Equations

• HCPolySupport.Book.Ch04.Internal.barBAtScaleOfPrimitive h = h.barB

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.Internal.barSigmaStarInvAtScaleOfPrimitive {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} (h : AnnealedPrimitiveScalarizationData P n) : ℝ

Internal scalar coefficient of the primitive inverse-star block.

Equations

• HCPolySupport.Book.Ch04.Internal.barSigmaStarInvAtScaleOfPrimitive h = h.barSigmaStarInv

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.Internal.annealedThetaAtScaleOfPrimitive {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} (h : AnnealedPrimitiveScalarizationData P n) : ℝ

Internal primitive contrast Theta_n.

Equations

• HCPolySupport.Book.Ch04.Internal.annealedThetaAtScaleOfPrimitive h = h.contrast