Lower bounds for the shifted-Laplacian energy form

The shifted Laplacian -Δ + m is a model for divergence-form energy estimates. The pointwise file TauCeti.Analysis.PDE.EnergyLowerBounds already proves that the jet density energyIntegrand 1 0 m U U has lower bound min 1 m * ‖U‖² for arbitrary real mass m. This file integrates that estimate for raw value-gradient jet fields.

These are still below the weak-derivative Sobolev-space layer: the inputs are arbitrary jet fields U : X → ℝ × EuclideanSpace ℝ n, and the statements carry the Bochner-integrability hypotheses needed to compare scalar integrals. Once H¹/W^{1,2} jets are available, these lemmas become the concrete coercive lower bounds for the shifted Dirichlet form.

Main declarations

• TauCeti.PDE.integral_min_one_mass_mul_norm_sq_le_energyFormIntegral_one_zero_mass_self: a variable real mass gives a lower bound with coefficient min 1 (m x).
• TauCeti.PDE.integral_min_one_const_mass_mul_norm_sq_le_energyFormIntegral_one_zero_mass_self: the constant-mass specialization.
• TauCeti.PDE.integral_norm_sq_le_energyFormIntegral_one_zero_mass_self_of_one_le: when the constant mass is at least 1, the shifted-Laplacian form controls the full jet norm with constant 1.
• TauCeti.PDE.energyFormIntegral_one_zero_zero_self_nonneg and TauCeti.PDE.energyFormIntegral_one_zero_mass_self_nonneg: nonnegativity of the Dirichlet and nonnegative shifted-Laplacian diagonal forms.

@[instance_reducible]

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

Local classical decidable equality for finite coordinate indices in shifted-Laplacian energy proofs.

Equations

• TauCeti.PDE.shiftedLaplacianEnergyDecidableEq = Classical.decEq n

theorem TauCeti.PDE.integral_min_one_mass_mul_norm_sq_le_energyFormIntegral_one_zero_mass_self {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] {μ : MeasureTheory.Measure X} {m : X → ℝ} {U : X → ℝ × EuclideanSpace ℝ n} (hlower : MeasureTheory.Integrable (fun (x : X) => min 1 (m x) * ‖U x‖ ^ 2) μ) (henergy : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand 1 0 (m x)) (U x)) (U x)) μ) : ∫ (x : X), min 1 (m x) * ‖U x‖ ^ 2 ∂μ ≤ energyFormIntegral μ (fun (x : X) => 1) (fun (x : X) => 0) m U U

Integrated diagonal lower bound for the shifted-Laplacian model with variable real mass.

Pointwise, energyIntegrand 1 0 (m x) (U x) (U x) is ‖(U x).2‖² + m x * (U x).1², which is bounded below by min 1 (m x) * ‖U x‖² even when m x is negative.

theorem TauCeti.PDE.energyFormIntegral_one_zero_mass_self_nonneg {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] {μ : MeasureTheory.Measure X} {m : X → ℝ} {U : X → ℝ × EuclideanSpace ℝ n} (hm : ∀ᵐ (x : X) ∂μ, 0 ≤ m x) : 0 ≤ energyFormIntegral μ (fun (x : X) => 1) (fun (x : X) => 0) m U U

The shifted-Laplacian diagonal form is nonnegative when the mass is a.e. nonnegative.

theorem TauCeti.PDE.energyFormIntegral_one_zero_zero_self_nonneg {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] {μ : MeasureTheory.Measure X} {U : X → ℝ × EuclideanSpace ℝ n} : 0 ≤ energyFormIntegral μ (fun (x : X) => 1) (fun (x : X) => 0) (fun (x : X) => 0) U U

The Dirichlet model -Δ has nonnegative diagonal energy.

theorem TauCeti.PDE.integral_min_one_const_mass_mul_norm_sq_le_energyFormIntegral_one_zero_mass_self {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] {μ : MeasureTheory.Measure X} {U : X → ℝ × EuclideanSpace ℝ n} {c : ℝ} (hlower : MeasureTheory.Integrable (fun (x : X) => min 1 c * ‖U x‖ ^ 2) μ) (henergy : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand 1 0 c) (U x)) (U x)) μ) : ∫ (x : X), min 1 c * ‖U x‖ ^ 2 ∂μ ≤ energyFormIntegral μ (fun (x : X) => 1) (fun (x : X) => 0) (fun (x : X) => c) U U

Constant-mass specialization of the integrated shifted-Laplacian lower bound.

theorem TauCeti.PDE.energyFormIntegral_one_zero_const_mass_self_nonneg {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] {μ : MeasureTheory.Measure X} {U : X → ℝ × EuclideanSpace ℝ n} {c : ℝ} (hc : 0 ≤ c) : 0 ≤ energyFormIntegral μ (fun (x : X) => 1) (fun (x : X) => 0) (fun (x : X) => c) U U

Constant nonnegative mass gives a nonnegative shifted-Laplacian diagonal form.

theorem TauCeti.PDE.integral_norm_sq_le_energyFormIntegral_one_zero_mass_self_of_one_le {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] {μ : MeasureTheory.Measure X} {U : X → ℝ × EuclideanSpace ℝ n} {c : ℝ} (hc : 1 ≤ c) (hlower : MeasureTheory.Integrable (fun (x : X) => ‖U x‖ ^ 2) μ) (henergy : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand 1 0 c) (U x)) (U x)) μ) : ∫ (x : X), ‖U x‖ ^ 2 ∂μ ≤ energyFormIntegral μ (fun (x : X) => 1) (fun (x : X) => 0) (fun (x : X) => c) U U

If the constant mass is at least 1, the shifted-Laplacian diagonal form controls the full raw jet L² density with constant 1.

theorem TauCeti.PDE.integral_norm_sq_le_energyFormIntegral_one_zero_one_self {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] {μ : MeasureTheory.Measure X} {U : X → ℝ × EuclideanSpace ℝ n} (hlower : MeasureTheory.Integrable (fun (x : X) => ‖U x‖ ^ 2) μ) (henergy : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand 1 0 1) (U x)) (U x)) μ) : ∫ (x : X), ‖U x‖ ^ 2 ∂μ ≤ energyFormIntegral μ (fun (x : X) => 1) (fun (x : X) => 0) (fun (x : X) => 1) U U

For constant mass 1, the shifted-Laplacian diagonal form controls the full raw jet L² density with constant 1.