The 2-energy of a density

The weighted 2-energy ∑ e, σ e * ρ e ^ 2 of a density, in both its ℝ≥0 form (Density.energy) and its real form on E → ℝ (Density.energyReal), together with the facts needed for the strong-duality argument: the energy is continuous and coercive, so it has compact sublevel sets over Density.toReal '' Γ.Adm and attains a minimum over a nonempty admissible set; strict convexity of the square makes the minimizer unique (FamilyOfObjects.existsUnique_isMinOn_energy).

noncomputable def Density.energy {E : Type u_1} (σ : E → NNReal) (ρ : Density E) : NNReal

The 2-energy of a density ρ with respect to the edge weights σ: ∑ e, σ e * ρ e ^ 2.

Equations

• Density.energy σ ρ = ∑ᶠ (e : E), σ e * ρ e ^ 2

noncomputable def Density.energyReal {E : Type u_1} [Fintype E] (σ : E → NNReal) (f : E → ℝ) : ℝ

The 2-energy with respect to the edge weights σ as a function of real-valued functions on E, for use with the real-analysis machinery. Agrees with Density.energy on coercions of densities (Density.energyReal_toReal).

Equations

• Density.energyReal σ f = ∑ e : E, ↑(σ e) * f e ^ 2

@[simp]

theorem Density.energyReal_apply {E : Type u_1} [Fintype E] (σ : E → NNReal) (f : E → ℝ) : energyReal σ f = ∑ e : E, ↑(σ e) * f e ^ 2

theorem Density.energyReal_toReal {E : Type u_1} [Fintype E] (σ : E → NNReal) (ρ : Density E) : energyReal σ ρ.toReal = ↑(energy σ ρ)

The real 2-energy of the coercion of a density is the coercion of its ℝ≥0 2-energy.

theorem Density.continuous_energyReal {E : Type u_1} [Fintype E] (σ : E → NNReal) : Continuous (energyReal σ)

The real 2-energy is continuous.

theorem Density.energyReal_nonneg {E : Type u_1} [Fintype E] (σ : E → NNReal) (f : E → ℝ) : 0 ≤ energyReal σ f

The real 2-energy is nonnegative.

theorem Density.length_mul_eq_energy {E : Type u_1} (σ : E → NNReal) (ρ : Density E) : length (σ * ρ) ρ = energy σ ρ

The 2-energy of a density is its length against the reweighted density σ * ρ.

theorem Density.energyReal_add_smul {E : Type u_1} [Fintype E] (σ : E → NNReal) (ρ : Density E) (f : E → ℝ) (t : ℝ) : energyReal σ (ρ.toReal + t • f) = energyReal σ ρ.toReal + 2 * t * (pairing (σ * ρ)) f + t ^ 2 * energyReal σ f

First-variation expansion of the real 2-energy at the coercion of a density ρ: moving by t • f changes the energy by a linear term, the pairing against the reweighted density σ * ρ, plus a quadratic remainder.

theorem Density.apply_le_sqrt_of_energyReal_le {E : Type u_1} [Fintype E] (σ : E → NNReal) (f : E → ℝ) (c : ℝ) (h : energyReal σ f ≤ c) (hσ : ∀ (e : E), 0 < σ e) (hf : ∀ (e : E), 0 ≤ f e) (e : E) : f e ≤ √(c / ↑(σ e))

If a nonnegative function f has 2-energy at most c with respect to strictly positive edge weights σ, then each coordinate satisfies f e ≤ √(c / σ e). This is the coercivity estimate that traps sublevel sets of the energy in a compact box.

theorem FamilyOfObjects.isCompact_sublevel_energy_toReal_image_adm {E : Type u_1} [Fintype E] (Γ : FamilyOfObjects E) (σ : E → NNReal) (hσ : ∀ (e : E), 0 < σ e) (c : ℝ) : IsCompact {f : E → ℝ | f ∈ Density.toReal '' Γ.Adm ∧ Density.energyReal σ f ≤ c}

Sublevel sets of the 2-energy with strictly positive edge weights σ, taken within the image of the admissible set, are compact: they are closed and trapped in the box ∏ e, [0, √(c / σ e)] by the coercivity estimate Density.apply_le_sqrt_of_energyReal_le.

theorem FamilyOfObjects.exists_isMinOn_energy {E : Type u_1} [Fintype E] (Γ : FamilyOfObjects E) (σ : E → NNReal) (hσ : ∀ (e : E), 0 < σ e) (hne : Γ.Adm.Nonempty) : ∃ ρ ∈ Γ.Adm, IsMinOn (Density.energy σ) Γ.Adm ρ

The 2-energy with strictly positive edge weights attains a minimum over a nonempty admissible set.

theorem FamilyOfObjects.existsUnique_isMinOn_energy {E : Type u_1} [Fintype E] (Γ : FamilyOfObjects E) (σ : E → NNReal) (hσ : ∀ (e : E), 0 < σ e) (hne : Γ.Adm.Nonempty) : ∃! ρ : Density E, ρ ∈ Γ.Adm ∧ IsMinOn (Density.energy σ) Γ.Adm ρ

Unique energy minimizer: over a nonempty admissible set, the 2-energy with strictly positive edge weights has exactly one minimizer. Existence is exists_isMinOn_energy; uniqueness holds because two distinct minimizers would average to an admissible density of strictly smaller energy.

theorem FamilyOfObjects.isMinOn_length_mul_of_isMinOn_energy {E : Type u_1} [Fintype E] (Γ : FamilyOfObjects E) (σ : E → NNReal) {ρs : Density E} (hρs : ρs ∈ Γ.Adm) (hMin : IsMinOn (Density.energy σ) Γ.Adm ρs) : IsMinOn (Density.length (σ * ρs)) Γ.Adm ρs

Variational inequality: a minimizer ρ* of the 2-energy over the admissible set also minimizes the linear functional γ ↦ (σ * ρ*).length γ over the admissible set. Moving from ρ* towards any admissible ρ changes the energy at first order by the pairing term of Density.energyReal_add_smul, which must therefore be nonnegative.