CapGeometry.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.cap_recession_component_lower line 16

Source documentation

A bounded cap quantitatively separates a unit recession direction from its horizontal hyperplane. This is the ray argument in bounds.tex:45–59.

theorem cap_recession_component_lower {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] {D : Set E} (ell : E →L[ℝ] ℝ) {b R ε : ℝ}
    (hR : 0 ≤ R) (hε : 0 < ε) (hcap : ∀ x ∈ D, ell x ≤ b → ‖x‖ ≤ R)
    {o e : E} (ho : o ∈ D) (hgap : ell o ≤ b-ε) (he : ‖e‖ = 1)
    (hrec : ∀ t : ℝ, 0 ≤ t → o+t • e ∈ D) :
    ε/(2*R+1) < ell e := by
…

theorem OAI.AffineBernstein.cap_normalized_vertical_bound line 38

Source documentation

The normalized vertical has uniformly bounded norm.

theorem cap_normalized_vertical_bound {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] {D : Set E} (ell : E →L[ℝ] ℝ) {b R ε : ℝ}
    (hR : 0 ≤ R) (hε : 0 < ε) (hcap : ∀ x ∈ D, ell x ≤ b → ‖x‖ ≤ R)
    {o e : E} (ho : o ∈ D) (hgap : ell o ≤ b-ε) (he : ‖e‖ = 1)
    (hrec : ∀ t : ℝ, 0 ≤ t → o+t • e ∈ D) :
    0 < ell e ∧ ell ((ell e)⁻¹ • e) = 1 ∧
      ‖(ell e)⁻¹ • e‖ ≤ (2*R+1)/ε := by
…

lemma OAI.AffineBernstein.isCompact_graph_sublevel_of_cap line 57
Source documentation
Compactness of a closed graph sublevel follows from compactness of the entire epigraph cap, without a boundary regularity hypothesis.
```
lemma isCompact_graph_sublevel_of_cap {n : ℕ} {Ω : Set (Space n)}
    {u : Space n → ℝ} {b : ℝ}
    (hK : IsCompact {p : Space n × ℝ | p.1 ∈ Ω ∧ u p.1 ≤ p.2 ∧ p.2 ≤ b}) :
    IsCompact {x | x ∈ Ω ∧ u x ≤ b} := by
…
```
Mentions: OAI.AffineBernstein.Space

lemma OAI.AffineBernstein.graph_ball_of_epigraph_ball line 73

Source documentation

The ambient ball supplies the graph's base ball at the center's height.

lemma graph_ball_of_epigraph_ball {n : ℕ} {Ω : Set (Space n)} {u : Space n → ℝ}
    {o : Space n × ℝ} {r : ℝ}
    (hball : Metric.ball o r ⊆ {p : Space n × ℝ | p.1 ∈ Ω ∧ u p.1 ≤ p.2}) :
    ∀ x ∈ Metric.ball o.1 r, x ∈ Ω ∧ u x ≤ o.2 := by
…

Mentions: OAI.AffineBernstein.Space

lemma OAI.AffineBernstein.graph_cap_radius_bound line 82

Source documentation

A cap radius bounds distances to the center in its base.

lemma graph_cap_radius_bound {n : ℕ} {Ω : Set (Space n)} {u : Space n → ℝ}
    {b R : ℝ} {c : Space n} (hc : ‖c‖ ≤ R)
    (hcap : ∀ p : Space n × ℝ, p.1 ∈ Ω → u p.1 ≤ p.2 → p.2 ≤ b → ‖p‖ ≤ R) :
    ∀ x, x ∈ Ω → u x < b → ‖x-c‖ ≤ 2*R := by
…

Mentions: OAI.AffineBernstein.Space