OAI/Analysis/AffineBernstein/CompletePositiveCap.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.sourceEpigraph_convex line 20
2. lemma OAI.AffineBernstein.sourceEpigraph_closed line 26
3. lemma OAI.AffineBernstein.sourceEpigraph_vertical_ray line 38
4. lemma OAI.AffineBernstein.affineEpigraphPullback_eq_image line 50
5. lemma OAI.AffineBernstein.affineEpigraphPullback_isClosed line 61
6. lemma OAI.AffineBernstein.affineEpigraphPullback_cap_vertical_pos line 68

   Source documentation

   A bounded literal epigraph cap forces its pulled vertical direction to have positive height. The cap center need only lie strictly below its top, so no global growth hypothesis is inserted.

   lemma affineEpigraphPullback_cap_vertical_pos {n : ℕ} {Ω : Set (Space n)} {u : Space n → ℝ}
       (a : Space n × ℝ) (L : (S × E) ≃L[ℝ] (Space n × ℝ)) (ℓ : S →L[ℝ] ℝ)
       {b R : ℝ} (hR : 0 ≤ R)
       (hcap : ∀ p ∈ affineEpigraphPullback Ω u a L, ℓ p.1 ≤ b → ‖p‖ ≤ R)
       {o : S × E} (ho : o ∈ affineEpigraphPullback Ω u a L) (hob : ℓ o.1 < b) :
       0 < ℓ (L.symm ((0:Space n),(1:ℝ))).1 := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.affineEpigraphPullback

7. lemma OAI.AffineBernstein.affineEpigraphPullback_graph_cap_data line 103

   Source documentation

   Actual compact original-graph cap data, derived from an ambient cap and its inner point. The lower height bound is explicit and uniform in the affine normalization.

   lemma affineEpigraphPullback_graph_cap_data {n : ℕ} {Ω : Set (Space n)} {u : Space n → ℝ}
       (hc : IsClosed (sourceEpigraph Ω u))
       (a : Space n × ℝ) (L : (S × E) ≃L[ℝ] (Space n × ℝ)) (ℓ : S →L[ℝ] ℝ)
       {b R : ℝ} (hR : 0 ≤ R)
       (hcap : ∀ p ∈ affineEpigraphPullback Ω u a L, ℓ p.1 ≤ b → ‖p‖ ≤ R)
       {o : S × E} (ho : o ∈ affineEpigraphPullback Ω u a L) (hob : ℓ o.1 < b) :
       ∃ K : Set (Space n), IsCompact K ∧ K ⊆ Ω ∧
         (∀ x ∈ Ω, x ∉ K → b ≤ pulledBaseGraphFunction u a L ℓ x) ∧
         (∀ x ∈ K, pulledBaseGraphFunction u a L ℓ x ∈ Icc (-‖ℓ‖*R) b) ∧
         (∀ x ∈ K, ‖L.symm ((x,u x)-a)‖ ≤ R) := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.sourceEpigraph, OAI.AffineBernstein.affineEpigraphPullback, OAI.AffineBernstein.pulledBaseGraphFunction

8. lemma OAI.AffineBernstein.affineEpigraphPullback_fiber_isCompact line 171

   Source documentation

   A cap containing a base fiber gives compactness of that actual fiber.

   lemma affineEpigraphPullback_fiber_isCompact {n : ℕ} {Ω : Set (Space n)} {u : Space n → ℝ}
       (hc : IsClosed (sourceEpigraph Ω u))
       (a : Space n × ℝ) (L : (S × E) ≃L[ℝ] (Space n × ℝ)) (ℓ : S →L[ℝ] ℝ)
       {b R : ℝ}
       (hcap : ∀ p ∈ affineEpigraphPullback Ω u a L, ℓ p.1 ≤ b → ‖p‖ ≤ R)
       {s : S} (hs : ℓ s ≤ b) : IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L} := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.sourceEpigraph, OAI.AffineBernstein.affineEpigraphPullback