Polarization

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Polarization on doubled vectors

Finite-dimensional algebra converting the diagonal of an arbitrary bilinear form on BlockVec d into its unique symmetric representing BlockMat d.

def Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.blockVecComp {d : ℕ} (P : HCPolySupport.BlockVec d) : HCPolySupport.BlockCoord d → ℝ

Coordinates of a block vector in the two-component basis.

Equations

• Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.blockVecComp P (Sum.inl i) = P.1 i
• Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.blockVecComp P (Sum.inr i) = P.2 i

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.blockVec_eq_sum_blockBasis {d : ℕ} (P : HCPolySupport.BlockVec d) : P = ∑ α : HCPolySupport.BlockCoord d, blockVecComp P α • HCPolySupport.blockBasis α

noncomputable def Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.blockQuadFormEntry {d : ℕ} (B : HCPolySupport.BlockVec d → ℝ) (α β : HCPolySupport.BlockCoord d) : ℝ

A polarized matrix entry reconstructed from a quadratic form.

Equations

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

noncomputable def Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.blockMatOfQuadForm {d : ℕ} (B : HCPolySupport.BlockVec d → ℝ) : HCPolySupport.BlockMat d

The block matrix reconstructed by polarizing a quadratic form.

Equations

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

@[simp]

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.blockMatEntry_blockMatOfQuadForm {d : ℕ} (B : HCPolySupport.BlockVec d → ℝ) (α β : HCPolySupport.BlockCoord d) : HCPolySupport.blockMatEntry (blockMatOfQuadForm B) α β = blockQuadFormEntry B α β

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.blockQuadFormEntry_symm {d : ℕ} (B : HCPolySupport.BlockVec d → ℝ) (α β : HCPolySupport.BlockCoord d) : blockQuadFormEntry B α β = blockQuadFormEntry B β α

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.isSymmetricBlockMat_blockMatOfQuadForm {d : ℕ} (B : HCPolySupport.BlockVec d → ℝ) : HCPolySupport.IsSymmetricBlockMat (blockMatOfQuadForm B)

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.sum_left {d : ℕ} (φ : HCPolySupport.BlockVec d → HCPolySupport.BlockVec d → ℝ) (hadd_l : ∀ (X Y Z : HCPolySupport.BlockVec d), φ (X + Y) Z = φ X Z + φ Y Z) (hsmul_l : ∀ (c : ℝ) (X Y : HCPolySupport.BlockVec d), φ (c • X) Y = c * φ X Y) {ι : Type u_1} (s : Finset ι) (f : ι → ℝ) (g : ι → HCPolySupport.BlockVec d) (Y : HCPolySupport.BlockVec d) : φ (∑ i ∈ s, f i • g i) Y = ∑ i ∈ s, f i * φ (g i) Y

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.sum_right {d : ℕ} (φ : HCPolySupport.BlockVec d → HCPolySupport.BlockVec d → ℝ) (hadd_r : ∀ (X Y Z : HCPolySupport.BlockVec d), φ X (Y + Z) = φ X Y + φ X Z) (hsmul_r : ∀ (c : ℝ) (X Y : HCPolySupport.BlockVec d), φ X (c • Y) = c * φ X Y) {ι : Type u_1} (s : Finset ι) (f : ι → ℝ) (g : ι → HCPolySupport.BlockVec d) (X : HCPolySupport.BlockVec d) : φ X (∑ i ∈ s, f i • g i) = ∑ i ∈ s, f i * φ X (g i)

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.bilin_apply_eq_sum {d : ℕ} (φ : HCPolySupport.BlockVec d → HCPolySupport.BlockVec d → ℝ) (hadd_l : ∀ (X Y Z : HCPolySupport.BlockVec d), φ (X + Y) Z = φ X Z + φ Y Z) (hsmul_l : ∀ (c : ℝ) (X Y : HCPolySupport.BlockVec d), φ (c • X) Y = c * φ X Y) (hadd_r : ∀ (X Y Z : HCPolySupport.BlockVec d), φ X (Y + Z) = φ X Y + φ X Z) (hsmul_r : ∀ (c : ℝ) (X Y : HCPolySupport.BlockVec d), φ X (c • Y) = c * φ X Y) (P Q : HCPolySupport.BlockVec d) : φ P Q = ∑ α : HCPolySupport.BlockCoord d, ∑ β : HCPolySupport.BlockCoord d, blockVecComp P α * blockVecComp Q β * φ (HCPolySupport.blockBasis α) (HCPolySupport.blockBasis β)

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.blockMatEntry_blockMatOfQuadForm_bilin {d : ℕ} (φ : HCPolySupport.BlockVec d → HCPolySupport.BlockVec d → ℝ) (hadd_l : ∀ (X Y Z : HCPolySupport.BlockVec d), φ (X + Y) Z = φ X Z + φ Y Z) (hadd_r : ∀ (X Y Z : HCPolySupport.BlockVec d), φ X (Y + Z) = φ X Y + φ X Z) (α β : HCPolySupport.BlockCoord d) : HCPolySupport.blockMatEntry (blockMatOfQuadForm fun (X : HCPolySupport.BlockVec d) => φ X X) α β = (φ (HCPolySupport.blockBasis α) (HCPolySupport.blockBasis β) + φ (HCPolySupport.blockBasis β) (HCPolySupport.blockBasis α)) / 2

theorem Algsuperdiff.Section24.CoarseMatrixDerivative.Internal.blockVecDot_blockMatVecMul_blockMatOfQuadForm_of_bilin {d : ℕ} (φ : HCPolySupport.BlockVec d → HCPolySupport.BlockVec d → ℝ) (hadd_l : ∀ (X Y Z : HCPolySupport.BlockVec d), φ (X + Y) Z = φ X Z + φ Y Z) (hsmul_l : ∀ (c : ℝ) (X Y : HCPolySupport.BlockVec d), φ (c • X) Y = c * φ X Y) (hadd_r : ∀ (X Y Z : HCPolySupport.BlockVec d), φ X (Y + Z) = φ X Y + φ X Z) (hsmul_r : ∀ (c : ℝ) (X Y : HCPolySupport.BlockVec d), φ X (c • Y) = c * φ X Y) (P : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot P (HCPolySupport.blockMatVecMul (blockMatOfQuadForm fun (X : HCPolySupport.BlockVec d) => φ X X) P) = φ P P