OAI/Analysis/AffineBernstein/AffineCapLIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.affineMaximal_uniform_affine_cap_lintegral_bound line 13

   Source documentation

   Original-PDE cap bound for the nonnegative integral used by actual chart transport. Integrability is produced from the compact cap data, not added as a hypothesis.

   theorem affineMaximal_uniform_affine_cap_lintegral_bound (n : ℕ)
       {ε r R : ℝ} (hε : 0 < ε) (hr : 0 < r) (hR : 0 ≤ R)
       (t₀ t₁ q₀ : ℝ) :
       ∃ C > 0, ∀ {Ω : Set (Space n)}, IsOpen Ω → Convex ℝ Ω →
         ∀ {u : Space n → ℝ}, ContDiffOn ℝ ∞ u Ω →
         (∀ x ∈ Ω, (hessian u x).PosDef) → AffineMaximalOn Ω u →
         ∀ (L : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (v : Space n × ℝ)
           (o : Space n) (c : ℝ) (a : Space n →L[ℝ] ℝ) (b d : ℝ),
         Metric.closedBall (L (o,c)+v) r ⊆ (fun p => L p+v) '' sourceEpigraph Ω u →
         a o+b*c+d = q₀ →
         ∀ {K Q : Set (Space n)}, IsCompact K → K ⊆ Ω → MeasurableSet Q → Q ⊆ K →
         (∀ x ∈ Ω, x ∉ K → t₁+ε ≤ graphAffineFunction u a b d x) →
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.sourceEpigraph, OAI.AffineBernstein.graphAffineFunction