Lower-order pointwise forms for divergence-form PDEs

For a divergence-form operator L u = -∂ⱼ(aⁱʲ ∂ᵢ u) + bⁱ ∂ᵢ u + c u, the principal matrix coefficient lives in TauCeti.Analysis.PDE.Ellipticity.Basic. This file records the two lower-order pointwise forms:

• u ↦ b(x) · ∇u, the first-order drift form driftForm (b x);
• u ↦ c(x) u, the zeroth-order mass form massForm (c x).

Boundedness of the coefficients is not given its own predicate: following Mathlib, a result that needs a bound states it inline, as ∀ x ∈ Ω, ‖b x‖ ≤ β, and the energy-form estimates in TauCeti.Analysis.PDE.EnergyForm.Basic and TauCeti.Analysis.PDE.EnergyLowerBounds take their bounds in that shape.

Main declarations

• TauCeti.PDE.driftForm, TauCeti.PDE.massForm: the pointwise lower-order forms.
• TauCeti.PDE.driftFormLinear: the drift coefficient-to-form map as a continuous linear map.
• TauCeti.PDE.massFormLinear: the mass coefficient-to-form map as a continuous linear map.
• TauCeti.PDE.norm_driftForm_apply_le and TauCeti.PDE.opNorm_driftForm_le.
• TauCeti.PDE.norm_massForm_apply_le and TauCeti.PDE.opNorm_massForm_le.
• Bound-by-a-constant and radius-restricted variants for both forms.

noncomputable def TauCeti.PDE.driftForm {n : Type u_1} [Fintype n] (b : EuclideanSpace ℝ n) : ℝ →L[ℝ] EuclideanSpace ℝ n →L[ℝ] ℝ

The pointwise first-order drift form (u, ξ) ↦ ⟪b, ξ⟫ u.

Equations

• TauCeti.PDE.driftForm b = (ContinuousLinearMap.smulRightL ℝ (EuclideanSpace ℝ n) ℝ) ((innerSL ℝ) b)

noncomputable def TauCeti.PDE.massForm (c : ℝ) : ℝ →L[ℝ] ℝ →L[ℝ] ℝ

The pointwise zeroth-order mass form (u, v) ↦ c u v.

Equations

• TauCeti.PDE.massForm c = c • ContinuousLinearMap.mul ℝ ℝ

@[simp]

theorem TauCeti.PDE.driftForm_apply {n : Type u_1} [Fintype n] (b : EuclideanSpace ℝ n) (u : ℝ) (ξ : EuclideanSpace ℝ n) : ((driftForm b) u) ξ = inner ℝ b ξ * u

Applying the drift form is the scalar product with the drift coefficient times u.

@[simp]

theorem TauCeti.PDE.massForm_apply (c u v : ℝ) : ((massForm c) u) v = c * u * v

Applying the mass form is multiplication by the mass coefficient.

Continuity in lower-order coefficients

noncomputable def TauCeti.PDE.driftFormLinear {n : Type u_1} [Fintype n] : EuclideanSpace ℝ n →L[ℝ] ℝ →L[ℝ] EuclideanSpace ℝ n →L[ℝ] ℝ

The drift coefficient-to-form map as a continuous linear map.

Equations

• TauCeti.PDE.driftFormLinear = ContinuousLinearMap.smulRightL ℝ (EuclideanSpace ℝ n) ℝ ∘SL innerSL ℝ

@[simp]

theorem TauCeti.PDE.driftFormLinear_apply {n : Type u_1} [Fintype n] (b : EuclideanSpace ℝ n) : driftFormLinear b = driftForm b

Applying driftFormLinear recovers driftForm.

theorem TauCeti.PDE.continuous_driftForm {n : Type u_1} [Fintype n] : Continuous fun (b : EuclideanSpace ℝ n) => driftForm b

The drift coefficient-to-form map is continuous.

noncomputable def TauCeti.PDE.massFormLinear : ℝ →L[ℝ] ℝ →L[ℝ] ℝ →L[ℝ] ℝ

The mass coefficient-to-form map as a continuous linear map.

Equations

• TauCeti.PDE.massFormLinear = ContinuousLinearMap.toSpanSingleton ℝ (ContinuousLinearMap.mul ℝ ℝ)

@[simp]

theorem TauCeti.PDE.massFormLinear_apply (c : ℝ) : massFormLinear c = massForm c

Applying massFormLinear recovers massForm.

theorem TauCeti.PDE.continuous_massForm : Continuous fun (c : ℝ) => massForm c

The mass coefficient-to-form map is continuous.

theorem TauCeti.PDE.Continuous.driftForm {n : Type u_1} [Fintype n] {X : Type u_2} [TopologicalSpace X] {b : X → EuclideanSpace ℝ n} (hb : Continuous b) : Continuous fun (x : X) => PDE.driftForm (b x)

A continuous drift coefficient field gives a continuous field of drift forms.

theorem TauCeti.PDE.Continuous.massForm {X : Type u_2} [TopologicalSpace X] {c : X → ℝ} (hc : Continuous c) : Continuous fun (x : X) => PDE.massForm (c x)

A continuous mass coefficient field gives a continuous field of mass forms.

theorem TauCeti.PDE.ContinuousOn.driftForm {n : Type u_1} [Fintype n] {X : Type u_2} [TopologicalSpace X] {s : Set X} {b : X → EuclideanSpace ℝ n} (hb : ContinuousOn b s) : ContinuousOn (fun (x : X) => PDE.driftForm (b x)) s

A continuous drift coefficient field on a set gives a continuous field of drift forms on that set.

theorem TauCeti.PDE.ContinuousOn.massForm {X : Type u_2} [TopologicalSpace X] {s : Set X} {c : X → ℝ} (hc : ContinuousOn c s) : ContinuousOn (fun (x : X) => PDE.massForm (c x)) s

A continuous mass coefficient field on a set gives a continuous field of mass forms on that set.

Drift form bounds

theorem TauCeti.PDE.norm_driftForm_apply_le {n : Type u_1} [Fintype n] (b : EuclideanSpace ℝ n) (u : ℝ) (ξ : EuclideanSpace ℝ n) : ‖((driftForm b) u) ξ‖ ≤ ‖b‖ * ‖u‖ * ‖ξ‖

The drift form is bounded by the norm of the drift coefficient.

theorem TauCeti.PDE.norm_driftForm_apply_le_of_norm_le {n : Type u_1} [Fintype n] {b : EuclideanSpace ℝ n} {β : ℝ} (hb : ‖b‖ ≤ β) (u : ℝ) (ξ : EuclideanSpace ℝ n) : ‖((driftForm b) u) ξ‖ ≤ β * ‖u‖ * ‖ξ‖

If the drift coefficient is bounded by β, then the drift form is bounded by β.

theorem TauCeti.PDE.opNorm_driftForm_le {n : Type u_1} [Fintype n] (b : EuclideanSpace ℝ n) : ‖driftForm b‖ ≤ ‖b‖

The operator norm of the drift form is bounded by the norm of the drift coefficient.

theorem TauCeti.PDE.opNorm_driftForm_le_of_norm_le {n : Type u_1} [Fintype n] {b : EuclideanSpace ℝ n} {β : ℝ} (hb : ‖b‖ ≤ β) : ‖driftForm b‖ ≤ β

If the drift coefficient is bounded by β, then the drift form has operator norm at most β.

theorem TauCeti.PDE.norm_driftForm_apply_le_of_norm_le_of_le {n : Type u_1} [Fintype n] {b : EuclideanSpace ℝ n} {β R S : ℝ} (hb : ‖b‖ ≤ β) {u : ℝ} {ξ : EuclideanSpace ℝ n} (hu : ‖u‖ ≤ R) (hξ : ‖ξ‖ ≤ S) : ‖((driftForm b) u) ξ‖ ≤ β * R * S

Radius-restricted drift estimate from a coefficient bound.

Mass form bounds

theorem TauCeti.PDE.norm_massForm_apply_le (c u v : ℝ) : ‖((massForm c) u) v‖ ≤ ‖c‖ * ‖u‖ * ‖v‖

The mass form is bounded by the norm of the mass coefficient.

theorem TauCeti.PDE.norm_massForm_apply_le_of_norm_le {c γ : ℝ} (hc : ‖c‖ ≤ γ) (u v : ℝ) : ‖((massForm c) u) v‖ ≤ γ * ‖u‖ * ‖v‖

If the mass coefficient is bounded by γ, then the mass form is bounded by γ.

theorem TauCeti.PDE.opNorm_massForm_le (c : ℝ) : ‖massForm c‖ ≤ ‖c‖

The operator norm of the mass form is bounded by the norm of the mass coefficient.

theorem TauCeti.PDE.opNorm_massForm_le_of_norm_le {c γ : ℝ} (hc : ‖c‖ ≤ γ) : ‖massForm c‖ ≤ γ

If the mass coefficient is bounded by γ, then the mass form has operator norm at most γ.

theorem TauCeti.PDE.norm_massForm_apply_le_of_norm_le_of_le {c γ R S : ℝ} (hc : ‖c‖ ≤ γ) {u v : ℝ} (hu : ‖u‖ ≤ R) (hv : ‖v‖ ≤ S) : ‖((massForm c) u) v‖ ≤ γ * R * S

Radius-restricted mass estimate from a coefficient bound.