OAI/Analysis/AffineBernstein/NormalizedCriticalDensity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.normalized_critical_density line 18

   Source documentation

   Uniform positive low-set measure, with no hidden ellipticity assumption.

   theorem normalized_critical_density {n : ℕ} (hn : 1 ≤ n) {ρ R : ℝ}
       (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hR : 1 ≤ R) :
       ∃ δ : ℝ, 0 < δ ∧ ∀ v : Space n → ℝ, BalancedNormalized ρ R v →
         ∀ s : Space n → ℝ, ContDiff ℝ ∞ s → (∀ x, 0 ≤ s x) →
         (∀ x, inverseHessianTrace v s x ≤ 0) → ∀ a ∈ Metric.ball (0:Space n) (1/64:ℝ),
         ∀ ε : ℝ, 0 < ε → s a ≤ ε →
         δ ≤ (volume {x | x ∈ Metric.closedBall (0:Space n) (1/16:ℝ) ∧ s x ≤ 2*ε}).toReal := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.BalancedNormalized, OAI.AffineBernstein.inverseHessianTrace