OAI/Analysis/AffineBernstein/UniformProductCap.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The first missing differential identity in sections/area.tex, Stationarity:
the cofactor of an actual Hessian is divergence-free. The proof below uses
multilinearity of the determinant and symmetry of second derivatives (Piola).
- theorem
OAI.AffineBernstein.affineMaximal_uniform_product_cap_lintegral_boundline 24Source documentation
The original PDE cap bound in literal base times flat-projective fiber coordinates. No measurability or integrability of the energy is assumed in this conversion.
theorem affineMaximal_uniform_product_cap_lintegral_bound {n : ℕ} (bS : OrthonormalBasis ι ℝ S) (bF : OrthonormalBasis κ ℝ F) (f : WithLp 2 (F × ℝ) ≃ₗᵢ[ℝ] E) (e : Fin n ≃ ι ⊕ κ) {ε r R : ℝ} (hε : 0 < ε) (hr : 0 < r) (hR : 0 ≤ R) (t₀ t₁ c₀ : ℝ) : ∃ C > 0, ∀ {Ω : Set (Space n)}, IsOpen Ω → Convex ℝ Ω → ∀ {u : Space n → ℝ}, ContDiffOn ℝ ∞ u Ω → (∀ x ∈ Ω, (hessian u x).PosDef) → AffineMaximalOn Ω u → ∀ (a : Space n × ℝ) (L : (S × E) ≃L[ℝ] (Space n × ℝ)) {B : Set S}, IsOpen B → (∀ s ∈ B, IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L}) → (∀ s ∈ B, (0:E) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L}) → ∀ (ℓ : S →L[ℝ] ℝ) (o : Space n) (c : ℝ), …Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.affineEpigraphPullback