OAI/Analysis/AffineBernstein/NoOrthant.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.exists_pos_mul_rpow_lt line 22
2. theorem OAI.AffineBernstein.affine_image_finite_strip_area line 35

   Source comment

   A finite union of actual affine-image thin strips obeys the sum of the source strip-area bounds, without a disjointness or integrability premise.

   theorem affine_image_finite_strip_area {n : ℕ} {Ω K : Set (Space n)}
       (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) (hK : MeasurableSet K) (hKΩ : K ⊆ Ω)
       {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
       (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
       (L : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (v : Space n × ℝ)
       {R ε : ℝ} (hR : 0 ≤ R) (hε : 0 < ε)
       (hxR : ∀ x ∈ K, ∀ i, |(L (x,u x)+v).1 i| ≤ R)
       (htR : ∀ x ∈ K, |(L (x,u x)+v).2| ≤ R)
       (hcover : ∀ x ∈ K, ∃ i : Fin n ⊕ Unit,
         |ambientCoordinates n (L (x,u x)+v) i| ≤ ε) :
       Real.rpow |L.toContinuousLinearMap.det| ((n:ℝ)/((n:ℝ)+2)) *
         (∫ x in K, affineAreaDensity u x) ≤
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.ambientCoordinates, OAI.AffineBernstein.affineAreaDensity

3. theorem OAI.AffineBernstein.complete_affineMaximal_no_orthant_limit line 77

   Source comment

   The m=0 case of bounds.tex is impossible for actual affine images of the complete affine-maximal graph. In particular the limit cannot be an orthant.

   theorem complete_affineMaximal_no_orthant_limit {n : ℕ} (hn : 0 < n)
       {Ω : Set (Space n)} (hΩ : IsOpen Ω) (hne : Ω.Nonempty) (hcv : Convex ℝ Ω)
       {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
       (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hm : AffineMaximalOn Ω u)
       (hc : EuclideanGraphComplete Ω u)
       (L : ℕ → (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (v : ℕ → Space n × ℝ) :
       ¬ LocalDistanceConverges (fun j => (fun z => L j z+v j) '' sourceEpigraph Ω u)
         (ambientOrthant n) := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.LocalDistanceConverges, OAI.AffineBernstein.sourceEpigraph, OAI.AffineBernstein.ambientOrthant