RationalCone.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Rational cones and extension of positive states on ordered groups.

def OAI.Kaplansky.orderedGroupRationalCone line 27
Source documentation
Positive fractions in the rational hull. A positive numerator may be chosen after multiplying numerator and denominator; no unperforation of G is assumed.
```
def orderedGroupRationalCone : PointedCone ℚ (DivisibleHull G) where
…
```
theorem OAI.Kaplansky.orderedGroupRationalCone_coe line 40
theorem OAI.Kaplansky.orderedGroupRationalCone_neg_unit line 45
Source documentation
A unit with no nonpositive positive multiple stays outside the negative of the rational cone, even if the group has torsion elsewhere.
```
theorem orderedGroupRationalCone_neg_unit (u : G)
    (hu : ∀ n : ℕ, 0 < n → ¬ n • u ≤ 0) :
    -(u : DivisibleHull G) ∉ orderedGroupRationalCone := by
…
```
Mentions: OAI.Kaplansky.orderedGroupRationalCone
theorem OAI.Kaplansky.orderedGroupRationalCone_unit_ne_zero line 58

theorem OAI.Kaplansky.orderedGroupRationalCone_unit_scalar line 66

Source documentation

Nonnegativity along the rational unit ray is reflected in its scalar.

theorem orderedGroupRationalCone_unit_scalar (u : G)
    (hu : ∀ n : ℕ, 0 < n → ¬ n • u ≤ 0) {q : ℚ}
    (hq : q • (u : DivisibleHull G) ∈ orderedGroupRationalCone) : 0 ≤ q := by
…

Mentions: OAI.Kaplansky.orderedGroupRationalCone

theorem OAI.Kaplansky.orderedGroupRationalCone_cofinal line 78
Source documentation
An order unit in G dominates every rational fraction after passage to the cone. The dominating vector is an integer multiple of the unit.
```
theorem orderedGroupRationalCone_cofinal (u : G) (hu : 0 ≤ u)
    (hb : ∀ g : G, ∃ N : ℕ, -(N • u) ≤ g) (x : DivisibleHull G) :
    ∃ N : ℕ, (N : ℚ) • (u : DivisibleHull G) + x ∈ orderedGroupRationalCone := by
…
```
Mentions: OAI.Kaplansky.orderedGroupRationalCone
theorem OAI.Kaplansky.RationalRieszExtension.step line 122
Source documentation
Induction step in M. Riesz extension theorem. Given a convex cone s in a vector space E, a partially defined linear map f : f.domain → ℝ, assume that f is nonnegative on f.domain ∩ p and p + s = E. If f is not defined on the whole E, then we can extend it to a larger submodule without breaking the non-negativity condition.
```
theorem step (nonneg : ∀ x : f.domain, (x : E) ∈ s → 0 ≤ f x)
    (dense : ∀ y, ∃ x : f.domain, (x : E) + y ∈ s) (hdom : f.domain ≠ ⊤) :
    ∃ g, f < g ∧ ∀ x : g.domain, (x : E) ∈ s → 0 ≤ g x := by
…
```
theorem OAI.Kaplansky.RationalRieszExtension.exists_top line 170
theorem OAI.Kaplansky.rational_riesz_extension line 202
Source documentation
M. Riesz extension theorem: given a convex cone s in a vector space E, a submodule p, and a linear f : p → ℝ, assume that f is nonnegative on p ∩ s and p + s = E. Then there exists a globally defined linear function g : E → ℝ that agrees with f on p, and is nonnegative on s.
```
theorem rational_riesz_extension (s : PointedCone ℚ E) (f : E →ₗ.[ℚ] ℝ)
    (nonneg : ∀ x : f.domain, (x : E) ∈ s → 0 ≤ f x)
    (dense : ∀ y, ∃ x : f.domain, (x : E) + y ∈ s) :
    ∃ g : E →ₗ[ℚ] ℝ, (∀ x : f.domain, g x = f x) ∧ ∀ x ∈ s, 0 ≤ g x := by
…
```
theorem OAI.Kaplansky.orderedGroup_normalized_state line 219
Source documentation
A normalized monotone real-valued additive state on an ordered group with an order unit. Positive unit multiples must not be nonpositive. Neither linear order nor unperforation of the group is assumed.
```
theorem orderedGroup_normalized_state (u : G) (hu : 0 ≤ u)
    (hn : ∀ n : ℕ, 0 < n → ¬ n • u ≤ 0)
    (hb : ∀ g : G, ∃ N : ℕ, -(N • u) ≤ g) :
    ∃ f : G →+ ℝ, Monotone f ∧ f u = 1 := by
…
```