Documentation

TauCeti.Analysis.PDE.EnergyForm.Continuity

Continuity of pointwise PDE energy integrands in the coefficients #

The finite-dimensional weak-form integrand energyIntegrand A b c is linear in the principal, drift, and mass coefficients. This file bundles that linearity as continuous linear maps from coefficient spaces to spaces of continuous bilinear maps.

This is a pointwise prerequisite for Lane D of the PDE roadmap. Once the weak energy form is defined by integrating x ↦ energyIntegrand (a x) (b x) (c x) over a domain, continuous coefficient fields and continuous perturbation families should give continuous integrand families without unfolding the jet form.

Main declarations #

source
noncomputable def TauCeti.PDE.energyIntegrandLinear {n : Type u_2} [Fintype n] :
Matrix n n ℝ × EuclideanSpace ℝ n × ℝ →L[ℝ] ℝ × EuclideanSpace ℝ n →L[ℝ] ℝ × EuclideanSpace ℝ n →L[ℝ] ℝ

The coefficient triple-to-energy-integrand map as a continuous linear map.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.PDE.energyIntegrandLinear_apply {n : Type u_2} [Fintype n] (A : Matrix n n ℝ) (b : EuclideanSpace ℝ n) (c : ℝ) :
    energyIntegrandLinear (A, b, c) = energyIntegrand A b c

    Applying energyIntegrandLinear recovers energyIntegrand for the coefficient triple.

    source
    theorem TauCeti.PDE.continuous_energyIntegrand {n : Type u_2} [Fintype n] :
    Continuous fun (p : Matrix n n ℝ × EuclideanSpace ℝ n × ℝ) => energyIntegrand p.1 p.2.1 p.2.2

    The full coefficient triple-to-energy-integrand map is continuous.

    source
    theorem TauCeti.PDE.Continuous.energyIntegrand {X : Type u_1} {n : Type u_2} [Fintype n] [TopologicalSpace X] {a : X → Matrix n n ℝ} {b : X → EuclideanSpace ℝ n} {c : X → ℝ} (ha : Continuous a) (hb : Continuous b) (hc : Continuous c) :
    Continuous fun (x : X) => PDE.energyIntegrand (a x) (b x) (c x)

    Continuous coefficient fields give a continuous field of full pointwise energy integrands.

    source
    theorem TauCeti.PDE.ContinuousOn.energyIntegrand {X : Type u_1} {n : Type u_2} [Fintype n] [TopologicalSpace X] {s : Set X} {a : X → Matrix n n ℝ} {b : X → EuclideanSpace ℝ n} {c : X → ℝ} (ha : ContinuousOn a s) (hb : ContinuousOn b s) (hc : ContinuousOn c s) :
    ContinuousOn (fun (x : X) => PDE.energyIntegrand (a x) (b x) (c x)) s

    Continuous coefficient fields on a set give a continuous field of full pointwise energy integrands on that set.