Cone.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Positive dual cones and their Laplace integrals (paper Piece 2, §01)

The measure is ordinary Lebesgue (statements proved for any compatible Lebesgue normalization where useful). "ProperCone" here is Mathlib's closed cone containing zero; the extra paper hypotheses (solid and contains no line) are imposed as needed. In the main application both C and its positive dual have specified interior points.

abbrev OAI.GeneralMahler.Rn line 22
Also declared: ComparatorChallenges/GeneralMahler.lean:12 (same declaration text).
abbrev OAI.GeneralMahler.posDual line 29
Source documentation
Paper C* = D.
```
abbrev posDual (C : ProperCone ℝ E) : ProperCone ℝ E :=
…
```
theorem OAI.GeneralMahler.mem_posDual line 33
theorem OAI.GeneralMahler.interior_dual_bound line 36
theorem OAI.GeneralMahler.interior_dual_of_bound line 53
theorem OAI.GeneralMahler.exists_ray_of_not_interior_dual line 72
Source documentation
If y is not interior to the dual, then there is a nonzero bad direction in the cone.
```
theorem exists_ray_of_not_interior_dual {C : ProperCone ℝ E} {y : E}
    (h : y ∉ interior (posDual C : Set E)) :
    ∃ x ∈ C, ‖x‖ = 1 ∧ ⟪y, x⟫ ≤ 0 := by
…
```
Mentions: OAI.GeneralMahler.posDual
def OAI.GeneralMahler.chi line 101
Source documentation
Paper §01 χ_C(V). Used with V interior to the dual.
```
def chi (C : ProperCone ℝ E) (V : E) : ℝ :=
…
```
def OAI.GeneralMahler.chiExt line 105
Source documentation
For limiting arguments keep track of infinity.
```
def chiExt (C : ProperCone ℝ E) (V : E) : ℝ≥0∞ :=
…
```
theorem OAI.GeneralMahler.integrable_polynomial_exp_tail line 111
Source documentation
Exponential tail with polynomial factors, finiteness. This elementary proof uses the integrable comparison (1+‖x‖)^(-r) above dimension r>n.
```
theorem integrable_polynomial_exp_tail {c : ℝ} (hc : 0 < c) (p : ℕ) :
    Integrable (fun x : E => (1 + ‖x‖)^p * Real.exp (-(c * ‖x‖))) := by
…
```
theorem OAI.GeneralMahler.chi_integrable line 140
theorem OAI.GeneralMahler.chi_pos line 151
theorem OAI.GeneralMahler.chiExt_eq line 160
theorem OAI.GeneralMahler.chiExt_lsc line 167
theorem OAI.GeneralMahler.chiExt_top line 182
Source documentation
If w has a bad direction in C, then the Laplace integral is infinite: translate C along that ray. The translated copy does not decrease the integral but misses a relatively low layer of positive volume measured in any interior-dual direction.
```
theorem chiExt_top {C : ProperCone ℝ E}
    (hs : (interior (C : Set E)).Nonempty)
    (hd : (interior (posDual C : Set E)).Nonempty)
    {V : E} (hV : V ∉ interior (posDual C : Set E)) :
    chiExt C V = ∞ := by
…
```
Mentions: OAI.GeneralMahler.posDual, OAI.GeneralMahler.chiExt
theorem OAI.GeneralMahler.chi_strictConvex line 250
Source documentation
Strict convexity on dual interior for a solid cone.
```
theorem chi_strictConvex {C : ProperCone ℝ E}
    (hs : (interior (C : Set E)).Nonempty) :
    StrictConvexOn ℝ (interior (posDual C : Set E)) (chi C) := by
…
```
Mentions: OAI.GeneralMahler.posDual, OAI.GeneralMahler.chi