WeightSamplingPolytope.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The compact polyhedron used for sampling the nilpotent boxes

theorem OAI.PolycyclicRecognition.SupportDatum.abs_weight_le_basisSupport line 20
Source documentation
Each balanced positive-multiplicity basis controls the absolute value of every generator weight, including its negative part.
```
theorem SupportDatum.abs_weight_le_basisSupport (D : SupportDatum W I B)
    (b : B) (i : I) (x : W) : |D.weight i x| ≤ D.basisSupport b x := by
…
```
Mentions: OAI.PolycyclicRecognition.SupportDatum
def OAI.PolycyclicRecognition.weightSamplingPolytope line 40
Source documentation
Halfspaces tangent to the unit ball, one per oriented generator ray.
```
def weightSamplingPolytope (α : I → W →L[ℝ] ℝ) : Set W :=
…
```
def OAI.PolycyclicRecognition.weightSamplingInterior line 44
Source documentation
Strict halfspaces give its interior sampling region.
```
def weightSamplingInterior (α : I → W →L[ℝ] ℝ) : Set W :=
…
```
theorem OAI.PolycyclicRecognition.isClosed_weightSamplingPolytope line 48
theorem OAI.PolycyclicRecognition.convex_weightSamplingPolytope line 54
theorem OAI.PolycyclicRecognition.convex_weightSamplingInterior line 60
theorem OAI.PolycyclicRecognition.isOpen_weightSamplingInterior line 66
theorem OAI.PolycyclicRecognition.weightSamplingInterior_subset_interior line 72

theorem OAI.PolycyclicRecognition.mem_smul_weightSamplingInterior line 81

Source documentation

Strict scaled facet inequalities place a point in the scaled interior.

theorem mem_smul_weightSamplingInterior (α : I → W →L[ℝ] ℝ)
    {a : ℝ} (ha : 0 < a) (x : W) (hx : ∀ i, α i x < a * ‖α i‖) :
    x ∈ (fun y : W => a • y) '' interior (weightSamplingPolytope α) := by
…

Mentions: OAI.PolycyclicRecognition.weightSamplingPolytope

theorem OAI.PolycyclicRecognition.closedBall_subset_weightSamplingPolytope line 91
theorem OAI.PolycyclicRecognition.zero_mem_weightSamplingInterior line 99
theorem OAI.PolycyclicRecognition.SupportDatum.isCompact_weightSamplingPolytope line 106
Source documentation
Positive balance and separation make the sampling polyhedron compact. No boundedness assumption on the polyhedron is needed.
```
theorem SupportDatum.isCompact_weightSamplingPolytope (D : SupportDatum W I B) (b : B) :
    IsCompact (weightSamplingPolytope (fun i => (D.weight i).toContinuousLinearMap)) := by
…
```
Mentions: OAI.PolycyclicRecognition.SupportDatum, OAI.PolycyclicRecognition.weightSamplingPolytope