OAI/Analysis/AffineBernstein/SupersolutionHighSet.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.normalized_supersolution_high_set_small line 21

   Source documentation

   A small value of a nonnegative supersolution forces almost all of the fixed inner ball below any prescribed positive threshold. The small value is quantitative and uniform in the generated normalized graph.

   theorem normalized_supersolution_high_set_small {n : ℕ} (hn : 1 ≤ n) {ρ R : ℝ}
       (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hR : 1 ≤ R) {η β : ℝ} (hη : 0 < η) (hβ : 0 < β) :
       ∃ ε : ℝ, 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:ℝ),
         s a ≤ ε → (volume {x | x ∈ Metric.closedBall (0:Space n) (1/16:ℝ) ∧ η ≤ s x}).toReal < β := by
   …

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