Symmetry of integrated zero-drift energy forms

Lane D of the PDE roadmap needs symmetric bilinear forms for the energy method and the Dirichlet spectrum. TauCeti.Analysis.PDE.SymmetricEnergy proves the corresponding finite-dimensional facts for the pointwise jet integrand. This file passes those facts through the Bochner integral for raw jet fields.

The statements remain below the weak-derivative Sobolev-space layer: the inputs are coefficient fields and raw value-gradient jets U V : X → ℝ × EuclideanSpace ℝ n. Once Lane A supplies Sobolev jets, these lemmas give the symmetric part of the weak form without unfolding the integrand.

Main declarations

• TauCeti.PDE.energyFormIntegral_zero_drift_transpose_apply: transposing the principal coefficient swaps the two jet fields under the integral.
• TauCeti.PDE.energyFormIntegral_zero_drift_comm_of_isSymm_ae: a.e. symmetric principal coefficients make the zero-drift integrated form symmetric.
• TauCeti.PDE.energyFormIntegral_zero_drift_swap_eq_of_isSymm_ae: bundled symmetry of the zero-drift integrated form under a.e. symmetric principal coefficients.
• TauCeti.PDE.energyFormIntegral_coefficientSymmetricPart_self: the diagonal integrated energy is unchanged by replacing the principal coefficient by its symmetric part.
• TauCeti.PDE.energyFormIntegral_coefficientSymmetricPart_zero_drift_apply: the symmetric-part zero-drift form is the average of the original form and its transpose, under the natural integrability hypotheses.

@[instance_reducible]

noncomputable def TauCeti.PDE.integratedSymmetricEnergyDecidableEq {n : Type u_2} : DecidableEq n

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

Equations

• TauCeti.PDE.integratedSymmetricEnergyDecidableEq = Classical.decEq n

theorem TauCeti.PDE.energyFormIntegral_zero_drift_transpose_apply {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] {μ : MeasureTheory.Measure X} {a : X → Matrix n n ℝ} {c : X → ℝ} {U V : X → ℝ × EuclideanSpace ℝ n} : energyFormIntegral μ (fun (x : X) => (a x).transpose) (fun (x : X) => 0) c U V = energyFormIntegral μ a (fun (x : X) => 0) c V U

With zero drift, transposing the principal coefficient swaps the two jet fields under the integral.

theorem TauCeti.PDE.energyFormIntegral_zero_drift_comm_of_isSymm_ae {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] {μ : MeasureTheory.Measure X} {a : X → Matrix n n ℝ} {c : X → ℝ} {U V : X → ℝ × EuclideanSpace ℝ n} (ha : ∀ᵐ (x : X) ∂μ, (a x).IsSymm) : energyFormIntegral μ a (fun (x : X) => 0) c U V = energyFormIntegral μ a (fun (x : X) => 0) c V U

A.e. symmetric principal coefficients make the zero-drift integrated energy form symmetric.

@[simp]

theorem TauCeti.PDE.energyFormIntegral_zero_drift_swap_eq_of_isSymm_ae {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] {μ : MeasureTheory.Measure X} {a : X → Matrix n n ℝ} {c : X → ℝ} (ha : ∀ᵐ (x : X) ∂μ, (a x).IsSymm) : Function.swap (energyFormIntegral μ a (fun (x : X) => 0) c) = energyFormIntegral μ a (fun (x : X) => 0) c

Bundled-map form of symmetry for a zero-drift integrated energy form with a.e. symmetric principal coefficients.

@[simp]

theorem TauCeti.PDE.energyFormIntegral_coefficientSymmetricPart_zero_drift_swap_eq {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] {μ : MeasureTheory.Measure X} {a : X → Matrix n n ℝ} {c : X → ℝ} : Function.swap (energyFormIntegral μ (fun (x : X) => coefficientSymmetricPart (a x)) (fun (x : X) => 0) c) = energyFormIntegral μ (fun (x : X) => coefficientSymmetricPart (a x)) (fun (x : X) => 0) c

Bundled-map symmetry for the symmetric-part zero-drift integrated energy form.

@[simp]

theorem TauCeti.PDE.energyFormIntegral_coefficientSymmetricPart_self {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] {μ : MeasureTheory.Measure X} {a : X → Matrix n n ℝ} {c : X → ℝ} {U : X → ℝ × EuclideanSpace ℝ n} {b : X → EuclideanSpace ℝ n} : energyFormIntegral μ (fun (x : X) => coefficientSymmetricPart (a x)) b c U U = energyFormIntegral μ a b c U U

Replacing the principal coefficient by its symmetric part does not change the diagonal integrated energy. The drift and mass coefficients are arbitrary, since the diagonal principal quadratic form is unchanged pointwise.

theorem TauCeti.PDE.energyFormIntegral_coefficientSymmetricPart_zero_drift_apply {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] {μ : MeasureTheory.Measure X} {a : X → Matrix n n ℝ} {c : X → ℝ} {U V : X → ℝ × EuclideanSpace ℝ n} (hUV : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) 0 (c x)) (U x)) (V x)) μ) (hVU : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) 0 (c x)) (V x)) (U x)) μ) : energyFormIntegral μ (fun (x : X) => coefficientSymmetricPart (a x)) (fun (x : X) => 0) c U V = (energyFormIntegral μ a (fun (x : X) => 0) c U V + energyFormIntegral μ a (fun (x : X) => 0) c V U) / 2

The symmetric-part zero-drift integrated form is the average of the original zero-drift form and its transpose, assuming the two original scalar densities are integrable.

theorem TauCeti.PDE.energyFormIntegral_coefficientSymmetricPart_eq_of_isSymm_ae {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] {μ : MeasureTheory.Measure X} {a : X → Matrix n n ℝ} {c : X → ℝ} {U V : X → ℝ × EuclideanSpace ℝ n} {b : X → EuclideanSpace ℝ n} (ha : ∀ᵐ (x : X) ∂μ, (a x).IsSymm) : energyFormIntegral μ (fun (x : X) => coefficientSymmetricPart (a x)) b c U V = energyFormIntegral μ a b c U V

For symmetric principal coefficients, replacing by the symmetric part leaves the integrated form unchanged.