OAI/Analysis/AffineBernstein/UniformSigmaCaps.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.complete_affineMaximal_uniform_sigma_bound line 18

   Source documentation

   A uniform weighted actual-sigma bound in a normalized positive cell. The cap energy, large minors and fiber area are all PRODUCED from literal geometry and the unchanged complete original PDE. In particular no integrability or energy bound is an assumption. All constants precede the varying graph and normalization.

   theorem complete_affineMaximal_uniform_sigma_bound {n k m d : ℕ}
       (hn : 1 ≤ n) (hk : 1 ≤ k) (hm : 1 ≤ m)
       (e : Fin n ≃ Fin k ⊕ Fin d) (eE : Fin m ≃ Fin d ⊕ Unit)
       (f : WithLp 2 (Space d × ℝ) ≃ₗᵢ[ℝ] Space m)
       {D Q : Set (Space k)} (hD : IsOpen D) (hDc : Convex ℝ D)
       (hQ : IsCompact Q) (hQD : Q ⊆ D)
       (o : Space k × Space m) {ε r₀ r₁ α ρ M R T RQ : ℝ}
       (hε : 0 < ε) (hr₀ : 0 < r₀) (hr₁ : 0 < r₁) (hα : 0 < α) (hρ : 0 < ρ)
       (hM : 0 ≤ M) (hR : 0 ≤ R)
       (hogap : ∀ j : Fin k, capTiltedForm j o.1 < T+ε)
       (hDheight : ∀ j : Fin k, ∀ s ∈ D, capTiltedForm j s ≤ T+ε)
       (hQheight : ∀ j : Fin k, ∀ s ∈ Q, capTiltedForm j s ≤ T-ε)
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.capTiltedForm