OAI/Analysis/AffineBernstein/DetCompactBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.affineMaximal_det_phase_bound line 21

   Source documentation

   Maximum-principle determinant upper estimate on a literal compact negative section. The compact section and gradient/depth bounds are geometric inputs; no Hessian, determinant, ellipticity or derivative bound is assumed.

   lemma affineMaximal_det_phase_bound {n : ℕ} {V Ω K : Set (Space n)}
       (hV : IsOpen V) (hΩ : IsOpen Ω) (hK : IsCompact K)
       (hΩK : Ω ⊆ K) (hKV : K ⊆ V) {u : Space n → ℝ}
       (hu : ContDiffOn ℝ ∞ u V) (hp : ∀ x ∈ V, (hessian u x).PosDef)
       (hm : AffineMaximalOn Ω u) (hneg : ∀ x ∈ Ω, u x < 0)
       (hbd : ∀ x ∈ K, x ∉ Ω → u x = 0)
       {γ M D : ℝ} (hγ : 0 < γ) (hM : 0 ≤ M) (hD : 0 ≤ D)
       (hsmall : γ*M ≤ 1/2) (hgrad : ∀ x ∈ Ω, gradientSquared u x ≤ M)
       (hdepth : ∀ x ∈ Ω, -u x ≤ D) {x : Space n} (hx : x ∈ Ω) :
       affineDetPhase u γ x ≤ (2*(n:ℝ)*(((n:ℝ)+2)/γ+M))^n * D^2 * Real.exp (γ*M/2) := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.gradientSquared, OAI.AffineBernstein.affineDetPhase

2. lemma OAI.AffineBernstein.affineDetPhase_ge_det_mul_depth line 52
3. lemma OAI.AffineBernstein.affineMaximal_det_upper_on_compact_section line 68