OrthogonalCoercivity

OrthogonalCoercivity

Terminal finite assembly scaffold. This file should expose one coercivity theorem and no new analytic content.

def DimdPolyLEAN.coeffPk {d : ℕ} (kappa : MultiIndex d) (H : Pkappa d kappa) (alpha : Idx d) : ℂ

coeffPk: coeff Pk.

Equations

• DimdPolyLEAN.coeffPk kappa H alpha = DimdPolyLEAN.coeffPkappa H alpha

def DimdPolyLEAN.OrthogonalToPk {d : ℕ} (kappa : MultiIndex d) (F G : Pkappa d kappa) : Prop

OrthogonalToPk: Orthogonal To Pk.

Equations

• DimdPolyLEAN.OrthogonalToPk kappa F G = DimdPolyLEAN.orthogonalToPk F G

noncomputable def DimdPolyLEAN.defectPk {d : ℕ} (kappa : MultiIndex d) (F G : Pkappa d kappa) : ℝ

defectPk: defect Pk.

Equations

• DimdPolyLEAN.defectPk kappa F G = DimdPolyLEAN.defect F G

noncomputable def DimdPolyLEAN.lowAnnulusMassPk {d : ℕ} (kappa : MultiIndex d) (J : ℕ) (H : Pkappa d kappa) : ℝ

lowAnnulusMassPk: low Annulus Mass Pk.

Equations

• DimdPolyLEAN.lowAnnulusMassPk kappa J H = DimdPolyLEAN.lowAnnulusMass J (DimdPolyLEAN.ofPkappa kappa H)

noncomputable def DimdPolyLEAN.highAnnulusMassPk {d : ℕ} (kappa : MultiIndex d) (J : ℕ) (H : Pkappa d kappa) : ℝ

highAnnulusMassPk: high Annulus Mass Pk.

Equations

• DimdPolyLEAN.highAnnulusMassPk kappa J H = DimdPolyLEAN.highAnnulusMass J (DimdPolyLEAN.ofPkappa kappa H)

theorem DimdPolyLEAN.orthogonal_coercivity {d : ℕ} (kappa : MultiIndex d) (hd : 0 < d) (F : Pkappa d kappa) (hF_ne : F ≠ 0) (hF_norm : ‖F‖ = 1) : ∃ (C_F_perp : ℝ), 0 < C_F_perp ∧ ∀ (G : Pkappa d kappa), OrthogonalToPk kappa F G → ‖G‖ ≤ C_F_perp * defectPk kappa F G