ConvexGeometry.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SymmetricMahler.zero_mem_interior_of_symmetric line 13

Source documentation

The center of an origin-symmetric convex set with interior is interior.

theorem zero_mem_interior_of_symmetric [Fintype I] [DecidableEq I] {K : Set (I → ℝ)} (hconv : Convex ℝ K)
    (hsym : ∀ x ∈ K, -x ∈ K) (hint : (interior K).Nonempty) :
    (0 : I → ℝ) ∈ interior K := by
…

theorem OAI.SymmetricMahler.exists_coordinate_rows line 22
Source documentation
Compactness supplies small nonzero coordinate rows in the polar.
```
theorem exists_coordinate_rows {K : Set (I → ℝ)} (hK : IsCompact K) :
    ∃ c : ℝ, 0 < c ∧ ∀ i : I, Pi.single i c ∈ coordinatePolar K := by
…
```
Mentions: OAI.SymmetricMahler.coordinatePolar
theorem OAI.SymmetricMahler.isClosed_stripBody line 35
Source documentation
Finite strip constraints form a closed set.
```
theorem isClosed_stripBody [Fintype J] [DecidableEq I] (A : J → I → ℝ) : IsClosed (stripBody A) := by
…
```
Mentions: OAI.SymmetricMahler.stripBody
def OAI.SymmetricMahler.approximationRows line 44
Source documentation
Independent coordinate rows followed by a finite prefix of polar rows.
```
def approximationRows (c : ℝ) (a : ℕ → I → ℝ) (N : ℕ) : (I ⊕ Fin N) → I → ℝ :=
…
```
lemma OAI.SymmetricMahler.approximationRows_basis line 47
lemma OAI.SymmetricMahler.approximationRows_sequence line 51
theorem OAI.SymmetricMahler.approximationRows_injective line 55
Source documentation
The first rows alone ensure full rank of every finite matrix.
```
theorem approximationRows_injective (c : ℝ) (hc : c ≠ 0) (a : ℕ → I → ℝ) (N : ℕ) :
    Function.Injective (measurement (approximationRows c a N)) := by
…
```
Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.approximationRows
lemma OAI.SymmetricMahler.stripBody_approximationRows_mem line 63
theorem OAI.SymmetricMahler.approximation_subset_box line 76
Source documentation
A single fixed coordinate box bounds every approximating strip body.
```
theorem approximation_subset_box {c : ℝ} (hc : 0 < c) (a : ℕ → I → ℝ) (N : ℕ) :
    stripBody (approximationRows c a N) ⊆ Icc (fun _ => -c⁻¹) (fun _ => c⁻¹) := by
…
```
Mentions: OAI.SymmetricMahler.stripBody, OAI.SymmetricMahler.approximationRows
theorem OAI.SymmetricMahler.isCompact_approximation line 87
lemma OAI.SymmetricMahler.approximation_antitone line 91
theorem OAI.SymmetricMahler.isCompact_coordinatePolar line 98
Source documentation
The polar of a symmetric body is bounded because K contains a ball.
```
theorem isCompact_coordinatePolar {K : Set (I → ℝ)}
    (hsym : ∀ x ∈ K, -x ∈ K) (hzero : (0 : I → ℝ) ∈ interior K) :
    IsCompact (coordinatePolar K) := by
…
```
Mentions: OAI.SymmetricMahler.coordinatePolar
lemma OAI.SymmetricMahler.subset_approximation line 120

theorem OAI.SymmetricMahler.iInter_approximation line 130

Source documentation

The common intersection is literally K, including the fixed initial rows.

theorem iInter_approximation {K : Set (I → ℝ)} (hconv : Convex ℝ K)
    (hclosed : IsClosed K) (hzero : (0 : I → ℝ) ∈ K) (hsym : ∀ x ∈ K, -x ∈ K)
    (c : ℝ) (hcK : ∀ i, Pi.single i c ∈ coordinatePolar K)
    (a : ℕ → coordinatePolar K) (ha : DenseRange a) :
    (⋂ N, stripBody (approximationRows c (fun j => (a j).val) N)) = K := by
…

Mentions: OAI.SymmetricMahler.coordinatePolar, OAI.SymmetricMahler.stripBody, OAI.SymmetricMahler.approximationRows