UniformSphericalCap.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.affineMaximal_uniform_spherical_cap_lintegral_bound line 29

Source documentation

Uniform full-sphere cap inverse energy, produced by the original affine maximal PDE. All angular charts, conormal multipliers and product measures are the actual ones, and constants are chosen before the varying normalized epigraph.

theorem affineMaximal_uniform_spherical_cap_lintegral_bound {n : ℕ}
    (bS : OrthonormalBasis ι ℝ S) (bF : OrthonormalBasis κ ℝ F)
    (bRef : OrthonormalBasis (κ ⊕ Unit) ℝ E)
    (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}) →
…

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

theorem OAI.AffineBernstein.enorm_sub_le_graphEDist line 106
Source comment
Every admissible graph path has at least the Euclidean length of its base displacement. This uses the literal C¹-path definition of completeness.
```
theorem enorm_sub_le_graphEDist {n : ℕ} (Ω : Set (Space n)) (u : Space n → ℝ)
    (x y : Space n) : ‖y - x‖ₑ ≤ graphEDist Ω u x y := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.graphEDist
theorem OAI.AffineBernstein.derivWithin_baseSegment line 131
Source comment
A straight base segment has constant velocity, including its endpoints for the closed-interval derivative used in the metric.
```
theorem derivWithin_baseSegment {n : ℕ} (x v : Space n) {t : ℝ}
    (ht : t ∈ Icc (0 : ℝ) 1) :
    derivWithin (fun s : ℝ => x + s • v) (Icc (0 : ℝ) 1) t = v := by
…
```
Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.graphEDist_le_of_segment_deriv_nonneg line 139

Source comment

Length estimate on a segment on which the graph height is nondecreasing.

theorem graphEDist_le_of_segment_deriv_nonneg {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (x y : Space n) (hseg : ∀ t ∈ Icc (0 : ℝ) 1, x + t • (y - x) ∈ Ω)
    (hp : ∀ t ∈ Icc (0 : ℝ) 1,
      0 ≤ fderiv ℝ u (x + t • (y - x)) (y - x)) :
    graphEDist Ω u x y ≤ ENNReal.ofReal (‖y - x‖ + (u y - u x)) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.graphEDist

theorem OAI.AffineBernstein.graphPathLength_neg line 204
Source comment
Coordinate entries coincide with the actual second Fréchet differential. The standing positive-Hessian hypothesis implies genuine convexity on the original open convex domain; this is not an additional hypothesis.
```
@[simp] theorem graphPathLength_neg {n : ℕ} (u : Space n → ℝ) (γ : ℝ → Space n) :
    graphPathLength (-u) γ = graphPathLength u γ := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.graphPathLength
theorem OAI.AffineBernstein.graphEDist_neg line 209

theorem OAI.AffineBernstein.graphEDist_le_segment_monotone line 216

Source comment

The straight-segment estimate in its geometric form. Both possible orientations of a monotone height are included.

theorem graphEDist_le_segment_monotone {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (x y : Space n) (hseg : ∀ t ∈ Icc (0 : ℝ) 1, x + t • (y - x) ∈ Ω)
    (hm : MonotoneOn (fun t : ℝ => u (x + t • (y - x))) (Icc (0 : ℝ) 1)) :
    graphEDist Ω u x y ≤ ENNReal.ofReal (‖y - x‖ + |u y - u x|) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.graphEDist

theorem OAI.AffineBernstein.graphEDist_le_segment_antitone line 233

theorem OAI.AffineBernstein.tendsto_of_graphEDist line 247

Source comment

Intrinsic convergence always entails convergence of base points.

theorem tendsto_of_graphEDist {n : ℕ} {Ω : Set (Space n)} {u : Space n → ℝ}
    {x : ℕ → Space n} {a : Space n}
    (ha : ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ i ≥ N,
      graphEDist Ω u (x i) a < ENNReal.ofReal ε) :
    Tendsto x atTop (𝓝 a) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.graphEDist

theorem OAI.AffineBernstein.mem_of_complete_graph_cauchy line 263

Source comment

Completeness prevents a finite base endpoint from being lost when graph paths make a sequence intrinsically Cauchy.

theorem mem_of_complete_graph_cauchy {n : ℕ} {Ω : Set (Space n)} {u : Space n → ℝ}
    (hc : EuclideanGraphComplete Ω u) {x : ℕ → Space n} {a : Space n}
    (hx : ∀ i, x i ∈ Ω) (ha : Tendsto x atTop (𝓝 a))
    (hC : ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ i ≥ N, ∀ j ≥ N,
      graphEDist Ω u (x i) (x j) < ENNReal.ofReal ε) : a ∈ Ω := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.graphEDist

theorem OAI.AffineBernstein.graph_cauchy_of_segment_bound line 273

Source comment

A chord bound along a family of segments turns ordinary Cauchy control of base and height into control for the actual graph metric.

theorem graph_cauchy_of_segment_bound {n : ℕ} {Ω : Set (Space n)} {u : Space n → ℝ}
    {x : ℕ → Space n} (hx : CauchySeq x) (hu : CauchySeq (u ∘ x))
    (hbound : ∀ i j, graphEDist Ω u (x i) (x j) ≤
      ENNReal.ofReal (‖x j - x i‖ + |u (x j) - u (x i)|)) :
    ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ i ≥ N, ∀ j ≥ N,
      graphEDist Ω u (x i) (x j) < ENNReal.ofReal ε := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.graphEDist

theorem OAI.AffineBernstein.graphEDist_le_on_monotone_ray line 294

Source comment

Restricting a monotone-height ray to any oriented subsegment gives the uniform chord bound used to exhibit an intrinsic Cauchy tail.

theorem graphEDist_le_on_monotone_ray {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (a v : Space n) (q : ℝ)
    (hseg : ∀ t ∈ Ico q 1, a + t • v ∈ Ω)
    (hm : MonotoneOn (fun t : ℝ => u (a + t • v)) (Ico q 1) ∨
      AntitoneOn (fun t : ℝ => u (a + t • v)) (Ico q 1))
    {s r : ℝ} (hs : s ∈ Ico q 1) (hr : r ∈ Ico q 1) :
    graphEDist Ω u (a + s • v) (a + r • v) ≤
      ENNReal.ofReal (‖(a + r • v) - (a + s • v)‖ +
        |u (a + r • v) - u (a + s • v)|) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.graphEDist

theorem OAI.AffineBernstein.endpoint_mem_of_bounded_monotone_ray line 340

Source comment

A bounded ray with monotone graph height cannot end at a missing finite base point of a complete graph. This proves the metric step rather than assuming properness of the embedding.

theorem endpoint_mem_of_bounded_monotone_ray {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hc : EuclideanGraphComplete Ω u) (a b : Space n) {q : ℝ} (hq : q < 1)
    (hseg : ∀ t ∈ Ico q 1, a + t • (b - a) ∈ Ω)
    (hm : MonotoneOn (fun t : ℝ => u (a + t • (b - a))) (Ico q 1) ∨
      AntitoneOn (fun t : ℝ => u (a + t • (b - a))) (Ico q 1))
    (hbdd : ∃ C : ℝ, ∀ t ∈ Ico q 1, |u (a + t • (b - a))| ≤ C) : b ∈ Ω := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.EuclideanGraphComplete

theorem OAI.AffineBernstein.convexOn_monotone_tail line 376

Source comment

A differentiable convex function on a finite half-open interval has a monotone tail (in one of the two orientations).

theorem convexOn_monotone_tail {f : ℝ → ℝ} (hf : ConvexOn ℝ (Ico (0 : ℝ) 1) f)
    (hd : ∀ t ∈ Ico (0 : ℝ) 1, DifferentiableAt ℝ f t) :
    ∃ q ∈ Ico (0 : ℝ) 1, MonotoneOn f (Ico q 1) ∨ AntitoneOn f (Ico q 1) := by
…

theorem OAI.AffineBernstein.convexOn_bounded_ray line 398

Source comment

The tangent line at the initial point bounds a convex ray from below, so an upper bound on a finite ray implies a two-sided bound.

theorem convexOn_bounded_ray {f : ℝ → ℝ} (hf : ConvexOn ℝ (Ico (0 : ℝ) 1) f)
    (hd : DifferentiableAt ℝ f 0) {A : ℝ} (hA : ∀ t ∈ Ico (0 : ℝ) 1, f t ≤ A) :
    ∃ C : ℝ, ∀ t ∈ Ico (0 : ℝ) 1, |f t| ≤ C := by
…

theorem OAI.AffineBernstein.endpoint_mem_of_bounded_convex_ray line 425

Source comment

Completeness forbids any bounded convex ray from reaching a missing finite endpoint. Convexity and two-sided variation, not a growth hypothesis, produce the required metric Cauchy sequence.

theorem endpoint_mem_of_bounded_convex_ray {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hcv : ConvexOn ℝ Ω u) (hc : EuclideanGraphComplete Ω u) (a b : Space n)
    (hseg : ∀ t ∈ Ico (0 : ℝ) 1, a + t • (b - a) ∈ Ω)
    (hbounded : ∃ A : ℝ, ∀ t ∈ Ico (0 : ℝ) 1, u (a + t • (b - a)) ≤ A) : b ∈ Ω := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.EuclideanGraphComplete

theorem OAI.AffineBernstein.mem_of_bounded_graph_sequence line 450

Source comment

The metric obstruction applied to an arbitrary bounded-height sequence, not merely points already lying on a fixed ray. This is the core boundary properness argument in geometry.tex:36–55.

theorem mem_of_bounded_graph_sequence {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hcv : ConvexOn ℝ Ω u) (hc : EuclideanGraphComplete Ω u)
    {a : Space n} (ha : a ∈ Ω) {x : ℕ → Space n} {b : Space n}
    (hx : ∀ i, x i ∈ Ω) (hlim : Tendsto x atTop (𝓝 b))
    {A : ℝ} (hA : ∀ i, u (x i) ≤ A) : b ∈ Ω := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.EuclideanGraphComplete

theorem OAI.AffineBernstein.isClosed_sublevel_of_complete line 486

Source comment

Actual height sublevels are closed in the ambient base space. No convex extension of u to missing boundary points is used.

theorem isClosed_sublevel_of_complete {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) (hne : Ω.Nonempty) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hcv : ConvexOn ℝ Ω u)
    (hc : EuclideanGraphComplete Ω u) (A : ℝ) :
    IsClosed {x | x ∈ Ω ∧ u x ≤ A} := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.EuclideanGraphComplete

theorem OAI.AffineBernstein.tendsto_atTop_at_boundary line 503

Source comment

Finite boundary blow-up, derived from the manuscript's literal Euclidean intrinsic completeness assumption.

theorem tendsto_atTop_at_boundary {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) (hne : Ω.Nonempty) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hcv : Convex ℝ Ω)
    (hpos : ∀ x ∈ Ω, (hessian u x).PosDef) (hc : EuclideanGraphComplete Ω u)
    {b : Space n} (hb : b ∉ Ω) : Tendsto u (𝓝[Ω] b) atTop := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.EuclideanGraphComplete

theorem OAI.AffineBernstein.isClosed_epigraph_of_complete line 519

Source comment

The epigraph is genuinely closed in Rⁿ × R. Completeness was not silently replaced by properness of the graph embedding.

theorem isClosed_epigraph_of_complete {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) (hne : Ω.Nonempty) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hcv : ConvexOn ℝ Ω u)
    (hc : EuclideanGraphComplete Ω u) :
    IsClosed {p : Space n × ℝ | p.1 ∈ Ω ∧ u p.1 ≤ p.2} := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.EuclideanGraphComplete