Coarse-graining support: Support.CoarseGraining.BlockFormalism.Properties

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

Block formalism -- block-state properties and admissibility

IsBlockPotentialOn / IsBlockPotentialZeroTraceOn / IsBlockSolenoidalOn / IsBlockSolenoidalZeroNormalTraceOn / IsBlockTestOn / BlockResponseSpace and IsBlockMuAdmissible definitions plus the IsBlockMuAdmissible namespace with its potentialCorrection / isPotentialZeroTrace bridges.

def HCPolySupport.IsBlockPotentialOn {d : ℕ} (U : Set (Vec d)) (X : BlockState d) : Prop

The potential component is the weak gradient of an H¹ function on U.

Equations

• HCPolySupport.IsBlockPotentialOn U X = HCPolySupport.IsPotentialOn U X.potential

def HCPolySupport.IsBlockPotentialZeroTraceOn {d : ℕ} (U : Set (Vec d)) (X : BlockState d) : Prop

The potential component is the weak gradient of an H¹₀ function on U.

Equations

• HCPolySupport.IsBlockPotentialZeroTraceOn U X = HCPolySupport.IsPotentialZeroTraceOn U X.potential

def HCPolySupport.IsBlockSolenoidalOn {d : ℕ} (U : Set (Vec d)) (X : BlockState d) : Prop

The flux pairs to zero with every weak gradient of an H¹₀(U) function.

Equations

• HCPolySupport.IsBlockSolenoidalOn U X = HCPolySupport.IsSolenoidalOn U X.flux

def HCPolySupport.IsBlockSolenoidalZeroNormalTraceOn {d : ℕ} (U : Set (Vec d)) (X : BlockState d) : Prop

The flux pairs to zero with every weak gradient of an H¹(U) function.

Equations

• HCPolySupport.IsBlockSolenoidalZeroNormalTraceOn U X = HCPolySupport.IsSolenoidalZeroNormalTraceOn U X.flux

def HCPolySupport.IsBlockTestOn {d : ℕ} (U : Set (Vec d)) (Y : BlockState d) : Prop

A block test state with an H¹₀ potential gradient and flux orthogonal to all H¹ gradients.

Equations

• HCPolySupport.IsBlockTestOn U Y = (HCPolySupport.IsBlockPotentialZeroTraceOn U Y ∧ HCPolySupport.IsBlockSolenoidalZeroNormalTraceOn U Y)

def HCPolySupport.BlockResponseSpace {d : ℕ} (a : CoeffField d) (U : Set (Vec d)) (X : BlockState d) : Prop

Potential and solenoidal components whose block coefficient pairing vanishes against every block test.

Equations

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

def HCPolySupport.IsBlockMuAdmissible {d : ℕ} (U : Set (Vec d)) (P : BlockVec d) (X : BlockState d) : Prop

Square-integrable deviations from P, with zero-trace potential and zero-normal-trace solenoidal flux.

Equations

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

theorem HCPolySupport.IsBlockMuAdmissible.potentialCorrection_memL2 {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {X : BlockState d} (hX : IsBlockMuAdmissible U P X) : MemVectorL2 U fun (x : Vec d) => X.potential x - P.1

theorem HCPolySupport.IsBlockMuAdmissible.isPotentialZeroTrace {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {X : BlockState d} (hX : IsBlockMuAdmissible U P X) : IsPotentialZeroTraceOn U fun (x : Vec d) => X.potential x - P.1

theorem HCPolySupport.IsBlockMuAdmissible.fluxCorrection_memL2 {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {X : BlockState d} (hX : IsBlockMuAdmissible U P X) : MemVectorL2 U fun (x : Vec d) => X.flux x - P.2

theorem HCPolySupport.IsBlockMuAdmissible.isSolenoidalZeroNormalTrace {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {X : BlockState d} (hX : IsBlockMuAdmissible U P X) : IsSolenoidalZeroNormalTraceOn U fun (x : Vec d) => X.flux x - P.2

noncomputable def HCPolySupport.blockEnergyDensity {d : ℕ} (a : CoeffField d) (X : BlockState d) (x : Vec d) : ℝ

One half of the quadratic block coefficient energy of the state at x.

Equations

• HCPolySupport.blockEnergyDensity a X x = 1 / 2 * HCPolySupport.blockVecDot (X.eval x) (HCPolySupport.blockMatVecMul (HCPolySupport.blockCoeffField a x) (X.eval x))

theorem HCPolySupport.blockEnergyDensity_ge_vecDot_of_isEllipticFieldOn {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) (X : BlockState d) {x : Vec d} (hx : x ∈ U) : vecDot (X.potential x) (X.flux x) ≤ blockEnergyDensity a X x

theorem HCPolySupport.blockEnergyDensity_matTranspose_flipFlux {d : ℕ} (a : CoeffField d) (X : BlockState d) (x : Vec d) : blockEnergyDensity (fun (y : Vec d) => matTranspose (a y)) X.flipFlux x = blockEnergyDensity a X x

theorem HCPolySupport.blockEnergyDensity_mapMatrix_conj_of_transpose_eq_self_of_mul_self_eq_one {d : ℕ} (a : CoeffField d) (X : BlockState d) (R : Mat d) (hR : matTranspose R = R) (hR2 : R * R = 1) (x : Vec d) : blockEnergyDensity (fun (y : Vec d) => R * a y * R) (BlockState.mapMatrix R X) x = blockEnergyDensity a X x

theorem HCPolySupport.blockEnergyDensity_mapMatrix_signFlipMatrix_conj {d : ℕ} (a : CoeffField d) (X : BlockState d) (i : Fin d) (x : Vec d) : blockEnergyDensity (fun (y : Vec d) => signFlipMatrix i * a y * signFlipMatrix i) (BlockState.mapMatrix (signFlipMatrix i) X) x = blockEnergyDensity a X x

theorem HCPolySupport.blockEnergyDensity_mapMatrix_swap_conj {d : ℕ} (a : CoeffField d) (X : BlockState d) (i j : Fin d) (x : Vec d) : blockEnergyDensity (fun (y : Vec d) => Matrix.swap ℝ i j * a y * Matrix.swap ℝ i j) (BlockState.mapMatrix (Matrix.swap ℝ i j) X) x = blockEnergyDensity a X x