Documentation

TauCeti.Analysis.PDE.SymmetricEnergy

Symmetric pointwise energy integrands #

For a divergence-form operator with no drift term, a symmetric principal coefficient matrix gives a symmetric pointwise jet bilinear form energyIntegrand A 0 c. This file records that finite-dimensional bookkeeping before the energy form is integrated over a Sobolev space.

The main use is Lane D of the PDE roadmap: the weak formulation and the Dirichlet spectrum need the integrated form coming from symmetric coefficients to be a symmetric coercive bilinear form. The already-existing coefficientSymmetricPart replaces a possibly nonsymmetric coefficient matrix by (A + Aᵀ) / 2; here we prove the corresponding facts for the full zero-drift jet integrand.

The quantitative diagonal lower bounds are supplied separately by TauCeti.Analysis.PDE.EnergyLowerBounds and its UniformlyEllipticOn wrappers. In the zero-drift case with positive mass and a principal quadratic lower bound, combine energyIntegrand_zero_drift_flip_eq_of_isSymm or energyIntegrand_coefficientSymmetricPart_zero_drift_flip_eq with min_lam_mass_mul_norm_sq_le_energyIntegrand_zero_drift_self rather than introducing a separate conjunction API.

Main declarations #

source
@[instance_reducible]
noncomputable def TauCeti.PDE.symmetricEnergyDecidableEq {n : Type u_1} :
DecidableEq n

Local classical decidable equality for finite coordinate indices in symmetry proofs.

Equations
Instances For
    source
    theorem TauCeti.PDE.energyIntegrand_zero_drift_transpose_apply {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) (c : ℝ) (U V : ℝ × EuclideanSpace ℝ n) :
    ((energyIntegrand A.transpose 0 c) U) V = ((energyIntegrand A 0 c) V) U

    With zero drift, transposing the principal coefficient swaps the two jet arguments.

    source
    theorem TauCeti.PDE.energyIntegrand_zero_drift_comm_of_isSymm {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} (hA : A.IsSymm) (c : ℝ) (U V : ℝ × EuclideanSpace ℝ n) :
    ((energyIntegrand A 0 c) U) V = ((energyIntegrand A 0 c) V) U

    A symmetric principal coefficient gives a symmetric zero-drift jet form.

    source
    @[simp]
    theorem TauCeti.PDE.energyIntegrand_zero_drift_flip_eq_of_isSymm {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} (hA : A.IsSymm) (c : ℝ) :
    (energyIntegrand A 0 c).flip = energyIntegrand A 0 c

    Bundled-map form of symmetry for the zero-drift jet integrand.

    Downstream energy forms that need the same integrand to be both symmetric and bounded below pair this with min_lam_mass_mul_norm_sq_le_energyIntegrand_zero_drift_self. For a nonsymmetric principal coefficient, first pass to coefficientSymmetricPart using the uniform ellipticity API in TauCeti.Analysis.PDE.Ellipticity.Basic, then apply this lemma to the symmetric coefficient field.

    source
    theorem TauCeti.PDE.energyIntegrand_coefficientSymmetricPart_zero_drift_apply {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) (c : ℝ) (U V : ℝ × EuclideanSpace ℝ n) :
    ((energyIntegrand (coefficientSymmetricPart A) 0 c) U) V = (((energyIntegrand A 0 c) U) V + ((energyIntegrand A 0 c) V) U) / 2

    The symmetric part's zero-drift jet form is the average of the original form and its transpose.

    source
    theorem TauCeti.PDE.energyIntegrand_coefficientSymmetricPart_self {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) (b : EuclideanSpace ℝ n) (c : ℝ) (U : ℝ × EuclideanSpace ℝ n) :
    ((energyIntegrand (coefficientSymmetricPart A) b c) U) U = ((energyIntegrand A b c) U) U

    Replacing the principal coefficient by its symmetric part does not change the diagonal energy density.

    source
    @[simp]
    theorem TauCeti.PDE.energyIntegrand_coefficientSymmetricPart_zero_drift_flip_eq {n : Type u_1} [Fintype n] (A : Matrix n n ℝ) (c : ℝ) :
    (energyIntegrand (coefficientSymmetricPart A) 0 c).flip = energyIntegrand (coefficientSymmetricPart A) 0 c

    Bundled-map form of symmetry for the symmetric-part zero-drift jet integrand.