Coarse-graining support: Support.CoarseGraining.MuQuadratic

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

noncomputable def HCPolySupport.blockPairingIntegrand {d : ℕ} (a : CoeffField d) (X Y : BlockState d) : Vec d → ℝ

The pointwise pairing of X with the block coefficient matrix applied to Y.

Equations

• HCPolySupport.blockPairingIntegrand a X Y x = HCPolySupport.blockVecDot (X.eval x) (HCPolySupport.blockMatVecMul (HCPolySupport.blockCoeffField a x) (Y.eval x))

noncomputable def HCPolySupport.blockEnergyAverage {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (X : BlockState d) : ℝ

The volume average of a block state's quadratic energy on U.

Equations

• HCPolySupport.blockEnergyAverage U a X = HCPolySupport.volumeAverage U (HCPolySupport.blockEnergyDensity a X)

noncomputable def HCPolySupport.blockPairingAverage {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (X Y : BlockState d) : ℝ

The volume average of the block coefficient pairing of two states on U.

Equations

• HCPolySupport.blockPairingAverage U a X Y = HCPolySupport.volumeAverage U (HCPolySupport.blockPairingIntegrand a X Y)

theorem HCPolySupport.blockPairingIntegrand_eq_hilbertInner {d : ℕ} (a : CoeffField d) (X Y : BlockState d) : blockPairingIntegrand a X Y = fun (x : Vec d) => inner ℝ (HilbertBlockVec.ofBlockVec (X.eval x)) ((HilbertBlockVec.applyBlockMat (blockCoeffField a x)) (HilbertBlockVec.ofBlockVec (Y.eval x)))

theorem HCPolySupport.blockEnergyAverage_eq_half_blockPairingAverage_self {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (X : BlockState d) : blockEnergyAverage U a X = 1 / 2 * blockPairingAverage U a X X

theorem HCPolySupport.blockEnergyDensity_eq_hilbertQuadratic {d : ℕ} (a : CoeffField d) (X : BlockState d) : blockEnergyDensity a X = fun (x : Vec d) => 1 / 2 * inner ℝ (HilbertBlockVec.ofBlockVec (X.eval x)) ((HilbertBlockVec.applyBlockMat (blockCoeffField a x)) (HilbertBlockVec.ofBlockVec (X.eval x)))

theorem HCPolySupport.blockPairingIntegrand_add_left {d : ℕ} (a : CoeffField d) (X Y Z : BlockState d) : blockPairingIntegrand a (X + Y) Z = fun (x : Vec d) => blockPairingIntegrand a X Z x + blockPairingIntegrand a Y Z x

theorem HCPolySupport.blockPairingIntegrand_add_right {d : ℕ} (a : CoeffField d) (X Y Z : BlockState d) : blockPairingIntegrand a X (Y + Z) = fun (x : Vec d) => blockPairingIntegrand a X Y x + blockPairingIntegrand a X Z x

theorem HCPolySupport.blockPairingIntegrand_smul_left {d : ℕ} (a : CoeffField d) (c : ℝ) (X Y : BlockState d) : blockPairingIntegrand a (c • X) Y = fun (x : Vec d) => c * blockPairingIntegrand a X Y x

theorem HCPolySupport.blockPairingIntegrand_smul_right {d : ℕ} (a : CoeffField d) (X Y : BlockState d) (c : ℝ) : blockPairingIntegrand a X (c • Y) = fun (x : Vec d) => c * blockPairingIntegrand a X Y x

theorem HCPolySupport.blockPairingAverage_add_left {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (X Y Z : BlockState d) (hXZ : MeasureTheory.IntegrableOn (blockPairingIntegrand a X Z) U MeasureTheory.volume) (hYZ : MeasureTheory.IntegrableOn (blockPairingIntegrand a Y Z) U MeasureTheory.volume) : blockPairingAverage U a (X + Y) Z = blockPairingAverage U a X Z + blockPairingAverage U a Y Z

theorem HCPolySupport.blockPairingAverage_add_right {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (X Y Z : BlockState d) (hXY : MeasureTheory.IntegrableOn (blockPairingIntegrand a X Y) U MeasureTheory.volume) (hXZ : MeasureTheory.IntegrableOn (blockPairingIntegrand a X Z) U MeasureTheory.volume) : blockPairingAverage U a X (Y + Z) = blockPairingAverage U a X Y + blockPairingAverage U a X Z

theorem HCPolySupport.blockPairingAverage_smul_left {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (c : ℝ) (X Y : BlockState d) : blockPairingAverage U a (c • X) Y = c * blockPairingAverage U a X Y

theorem HCPolySupport.blockPairingAverage_smul_right {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (X Y : BlockState d) (c : ℝ) : blockPairingAverage U a X (c • Y) = c * blockPairingAverage U a X Y

structure HCPolySupport.LinearMuMinimizerFamily {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : Type

A linear family of minimizers for the doubled μ-problem. This isolates the analytic content of the notes: once such a family is available, μ(U,·;a) is automatically quadratic, hence the coarse block matrix exists canonically.

• field : BlockVec d → BlockState d

  The linear family of admissible block states realizing the minimum energy for each constant pair.

• map_add (P Q : BlockVec d) : self.field (P + Q) = self.field P + self.field Q
• map_smul (c : ℝ) (P : BlockVec d) : self.field (c • P) = c • self.field P
• admissible (P : BlockVec d) : IsBlockMuAdmissible U P (self.field P)
• pairingIntegrable (P Q : BlockVec d) : MeasureTheory.IntegrableOn (blockPairingIntegrand a (self.field P) (self.field Q)) U MeasureTheory.volume
• realizes (P : BlockVec d) : Mu U P a = blockEnergyAverage U a (self.field P)

noncomputable def HCPolySupport.LinearMuMinimizerFamily.toBilin {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (F : LinearMuMinimizerFamily U a) : FullBlockVec d →ₗ[ℝ] FullBlockVec d →ₗ[ℝ] ℝ

The bilinear form obtained by averaging coefficient pairings of the family's minimizing states.

Equations

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

noncomputable def HCPolySupport.LinearMuMinimizerFamily.quadraticForm {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (F : LinearMuMinimizerFamily U a) : QuadraticForm ℝ (FullBlockVec d)

The quadratic form obtained by pairing each minimizing state with itself.

Equations

• F.quadraticForm = LinearMap.BilinMap.toQuadraticMap F.toBilin

theorem HCPolySupport.LinearMuMinimizerFamily.quadraticForm_apply {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (F : LinearMuMinimizerFamily U a) (P : BlockVec d) : F.quadraticForm (toFullBlockVec P) = blockPairingAverage U a (F.field P) (F.field P)

theorem HCPolySupport.LinearMuMinimizerFamily.hasQuadraticMu {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (F : LinearMuMinimizerFamily U a) : HasQuadraticMu U a

theorem HCPolySupport.LinearMuMinimizerFamily.exists_coarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (F : LinearMuMinimizerFamily U a) : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix U a Abar

theorem HCPolySupport.LinearMuMinimizerFamily.existsUnique_coarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (F : LinearMuMinimizerFamily U a) : ∃! Abar : BlockMat d, IsCoarseBlockMatrix U a Abar

theorem HCPolySupport.LinearMuMinimizerFamily.mu_eq_half_blockVecDot_coarseBlockMatrix {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (F : LinearMuMinimizerFamily U a) (P : BlockVec d) : Mu U P a = 1 / 2 * blockVecDot P (blockMatVecMul (coarseBlockMatrix U a) P)