MatrixConcavity.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.det_rpow_le_one_add_trace line 18
Source documentation
Weighted arithmetic-geometric mean for the eigenvalues, with the unused weight placed at 1. This is the determinant-power supporting inequality at I.
```
theorem det_rpow_le_one_add_trace {n : ℕ} {H : Matrix (Fin n) (Fin n) ℝ}
    (hH : H.PosSemidef) {δ : ℝ} (hδ : 0 ≤ δ) (hnδ : (n : ℝ) * δ ≤ 1) :
    H.det ^ δ ≤ 1 + δ * (H.trace - n) := by
…
```

theorem OAI.AffineBernstein.exists_normalized_posSemidef line 48

Source documentation

Congruence by the inverse positive square root converts the determinant ratio and the mixed trace to the same positive semidefinite matrix.

theorem exists_normalized_posSemidef {n : ℕ} {A B : Matrix (Fin n) (Fin n) ℝ}
    (hA : A.PosDef) (hB : B.PosSemidef) :
    ∃ C : Matrix (Fin n) (Fin n) ℝ, C.PosSemidef ∧
      C.det = B.det / A.det ∧ C.trace = (A⁻¹ * B).trace := by
…

theorem OAI.AffineBernstein.det_rpow_tangent_inequality line 69

Source documentation

Concavity in its precise tangent form, for all exponents in [0,1/n].

theorem det_rpow_tangent_inequality {n : ℕ} {A B : Matrix (Fin n) (Fin n) ℝ}
    (hA : A.PosDef) (hB : B.PosSemidef) {δ : ℝ} (hδ : 0 ≤ δ)
    (hnδ : (n : ℝ) * δ ≤ 1) :
    B.det ^ δ ≤ A.det ^ δ + δ * A.det ^ δ * (A⁻¹ * (B - A)).trace := by
…

theorem OAI.AffineBernstein.hessian_add_on line 91

Source documentation

On an open set the Hessian is additive; no extension outside that set is used.

theorem hessian_add_on {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {u v : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω) (hv : ContDiffOn ℝ ∞ v Ω)
    {x : Space n} (hx : x ∈ Ω) :
    hessian (fun y => u y + v y) x = hessian u x + hessian v x := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian

theorem OAI.AffineBernstein.hessian_isSymm line 114
theorem OAI.AffineBernstein.matrix_trace_pair line 119

theorem OAI.AffineBernstein.affineArea_tangent_inequality line 129

Source documentation

The actual determinant density obeys its supporting-hyperplane inequality.

theorem affineArea_tangent_inequality {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {u η : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω) (hη : ContDiffOn ℝ ∞ η Ω)
    {x : Space n} (hx : x ∈ Ω) (hpos : (hessian u x).PosDef)
    (hpert : (hessian (fun y => u y + η y) x).PosSemidef) :
    affineAreaDensity (fun y => u y + η y) x - affineAreaDensity u x ≤
      (1 / ((n : ℝ) + 2)) * (affineAreaDensity u x *
        (∑ i, ∑ j, (hessian u x)⁻¹ i j * hessian η x i j)) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.affineAreaDensity

theorem OAI.AffineBernstein.integrableOn_affineArea_difference line 152

Source documentation

Density differences for a compactly supported perturbation really are integrable, although each area on an unbounded domain could be infinite.

theorem integrableOn_affineArea_difference {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hpos : ∀ y ∈ Ω, (hessian u y).PosDef)
    (η : Space n → ℝ) (hη : ContDiff ℝ ∞ η) (hηc : HasCompactSupport η)
    (hηΩ : tsupport η ⊆ Ω)
    (hpert : ∀ y ∈ Ω, (hessian (fun z => u z + η z) y).PosDef) :
    IntegrableOn (fun x => affineAreaDensity (fun y => u y + η y) x - affineAreaDensity u x) Ω := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.affineAreaDensity

theorem OAI.AffineBernstein.affineMaximal_local_area_maximization line 179

Source documentation

Local maximization of graph affine area, deduced from the PDE rather than assumed as stability.

theorem affineMaximal_local_area_maximization {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hpos : ∀ y ∈ Ω, (hessian u y).PosDef) (hmax : AffineMaximalOn Ω u)
    (η : Space n → ℝ) (hη : ContDiff ℝ ∞ η) (hηc : HasCompactSupport η)
    (hηΩ : tsupport η ⊆ Ω)
    (hpert : ∀ y ∈ Ω, (hessian (fun z => u z + η z) y).PosDef) :
    (∫ x in Ω, affineAreaDensity (fun y => u y + η y) x - affineAreaDensity u x) ≤ 0 := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.affineAreaDensity

def OAI.AffineBernstein.affineBaseMap line 199
Source documentation
The affine pullback uses the continuous map associated with the actual matrix, so its determinant and nonsingularity have their usual meanings.
```
def affineBaseMap {n : ℕ} (B : Matrix (Fin n) (Fin n) ℝ) (d : Space n) (y : Space n) : Space n :=
…
```
Mentions: OAI.AffineBernstein.Space
theorem OAI.AffineBernstein.euclideanCLM_coordinateVector line 202

theorem OAI.AffineBernstein.dirDeriv_comp_affine line 208

Source documentation

First derivative of composition with an affine base change.

theorem dirDeriv_comp_affine {n : ℕ} (B : Matrix (Fin n) (Fin n) ℝ) (d : Space n)
    {u : Space n → ℝ} {x : Space n} (hu : DifferentiableAt ℝ u (affineBaseMap B d x))
    (v : Space n) :
    dirDeriv v (fun y => u (affineBaseMap B d y)) x =
      dirDeriv (Matrix.toEuclideanCLM (𝕜 := ℝ) (n := Fin n) B v) u (affineBaseMap B d x) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.affineBaseMap, OAI.AffineBernstein.dirDeriv

theorem OAI.AffineBernstein.hessian_comp_affine line 220

Source documentation

The Hessian chain rule, retaining the exact order Bᵀ H B.

theorem hessian_comp_affine {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (B : Matrix (Fin n) (Fin n) ℝ) (d : Space n) {x : Space n}
    (hx : affineBaseMap B d x ∈ Ω) :
    hessian (fun y => u (affineBaseMap B d y)) x =
      B.transpose * hessian u (affineBaseMap B d x) * B := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.affineBaseMap, OAI.AffineBernstein.hessian

theorem OAI.AffineBernstein.hessian_const_mul line 257

Source documentation

Multiplying heights by a scalar multiplies the actual Hessian by it.

theorem hessian_const_mul {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω) (c : ℝ) {x : Space n} (hx : x ∈ Ω) :
    hessian (fun y => c * u y) x = c • hessian u x := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian

theorem OAI.AffineBernstein.posDef_affine_congruence line 273
Source documentation
Nonsingular congruence and positive scalar multiplication preserve strict ellipticity. The condition on B is exactly invertibility, not orthogonality.
```
theorem posDef_affine_congruence {n : ℕ} {H B : Matrix (Fin n) (Fin n) ℝ}
    (hH : H.PosDef) (hB : B.det ≠ 0) {c : ℝ} (hc : 0 < c) :
    (c • (B.transpose * H * B)).PosDef := by
…
```

theorem OAI.AffineBernstein.det_affine_congruence line 282

Source documentation

Exact determinant normalization used for rescaled sections.

theorem det_affine_congruence {n : ℕ} (H B : Matrix (Fin n) (Fin n) ℝ) (c : ℝ) :
    (c • (B.transpose * H * B)).det = (c ^ n * B.det ^ 2) * H.det := by
…

theorem OAI.AffineBernstein.trace_inverse_congruence line 289

Source documentation

The trace contraction is invariant under simultaneous congruence, with the exact scalar ratio. This is the algebra behind covariance of the affine PDE.

theorem trace_inverse_congruence {n : ℕ} {H B : Matrix (Fin n) (Fin n) ℝ}
    (hH : H.PosDef) (hB : B.det ≠ 0) {c : ℝ} (hc : 0 < c)
    (K : Matrix (Fin n) (Fin n) ℝ) (t : ℝ) :
    ((c • (B.transpose * H * B))⁻¹ * (t • (B.transpose * K * B))).trace =
    (c⁻¹ * t) * (H⁻¹ * K).trace := by
…

theorem OAI.AffineBernstein.affineMaximalOn_iff_trace line 315
Source documentation
The classical PDE is equivalent to the inverse-Hessian trace formulation wherever its coefficients are the actual positive-definite Hessian.
```
theorem affineMaximalOn_iff_trace {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hpos : ∀ y ∈ Ω, (hessian u y).PosDef) :
    AffineMaximalOn Ω u ↔ ∀ x ∈ Ω,
      ((hessian u x)⁻¹ * hessian (affineWeight u) x).trace = 0 := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.affineWeight
def OAI.AffineBernstein.affineGraphPullback line 330
Source documentation
Change of base variables, positive vertical scaling, and arbitrary affine height correction. This includes the normalization of sections in rigidity.
```
def affineGraphPullback {n : ℕ} (u : Space n → ℝ) (B : Matrix (Fin n) (Fin n) ℝ)
    (d : Space n) (a : Space n →L[ℝ] ℝ) (c e : ℝ) : Space n → ℝ :=
…
```
Mentions: OAI.AffineBernstein.Space
theorem OAI.AffineBernstein.contDiff_affineBaseMap line 334
theorem OAI.AffineBernstein.contDiffOn_affineGraphPullback line 338
theorem OAI.AffineBernstein.hessian_affineGraphPullback line 345
theorem OAI.AffineBernstein.posDef_hessian_affineGraphPullback line 359

theorem OAI.AffineBernstein.affineWeight_affineGraphPullback line 370

Source documentation

The actual determinant weight transforms by its exact positive constant.

theorem affineWeight_affineGraphPullback {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hpos : ∀ y ∈ Ω, (hessian u y).PosDef)
    {B : Matrix (Fin n) (Fin n) ℝ} (hB : B.det ≠ 0) (d : Space n)
    (a : Space n →L[ℝ] ℝ) {c : ℝ} (hc : 0 < c) (e : ℝ)
    {x : Space n} (hx : affineBaseMap B d x ∈ Ω) :
    affineWeight (affineGraphPullback u B d a c e) x =
      Real.rpow (c ^ n * B.det ^ 2) (-(((n : ℝ) + 1) / ((n : ℝ) + 2))) *
        affineWeight u (affineBaseMap B d x) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.affineBaseMap, OAI.AffineBernstein.affineWeight, OAI.AffineBernstein.affineGraphPullback

theorem OAI.AffineBernstein.hessian_congr_nhds line 385
Source documentation
Hessians are local, including their inner derivative.
```
theorem hessian_congr_nhds {n : ℕ} {u v : Space n → ℝ} {x : Space n}
    (he : u =ᶠ[nhds x] v) : hessian u x = hessian v x := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian

theorem OAI.AffineBernstein.affineMaximalOn_affineGraphPullback line 396

Source documentation

Exact, classical affine-maximal PDE covariance for section normalization. No transformed PDE is assumed: it follows from the original one by the actual Hessian and determinant chain rules.

theorem affineMaximalOn_affineGraphPullback {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hpos : ∀ y ∈ Ω, (hessian u y).PosDef) (hmax : AffineMaximalOn Ω u)
    {B : Matrix (Fin n) (Fin n) ℝ} (hB : B.det ≠ 0) (d : Space n)
    (a : Space n →L[ℝ] ℝ) {c : ℝ} (hc : 0 < c) (e : ℝ) :
    AffineMaximalOn (affineBaseMap B d ⁻¹' Ω) (affineGraphPullback u B d a c e) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.affineBaseMap, OAI.AffineBernstein.affineGraphPullback