WeightSamplingSupport.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact positive widths of the sampling polytope

theorem OAI.PolycyclicRecognition.weightSampling_support_eq_norm line 15

Source documentation

Every defining halfspace is attained at its Euclidean contact point.

theorem weightSampling_support_eq_norm
    {W I : Type*} [NormedAddCommGroup W] [InnerProductSpace ℝ W]
    [FiniteDimensional ℝ W] [Fintype I]
    (α : I → W →L[ℝ] ℝ) (hC : IsCompact (weightSamplingPolytope α))
    (i : I) (hi : α i ≠ 0) :
    sSup (α i '' weightSamplingPolytope α) = ‖α i‖ := by
…

Mentions: OAI.PolycyclicRecognition.weightSamplingPolytope

theorem OAI.PolycyclicRecognition.bracketWordExponent_pos line 33
Source documentation
Every nonempty bracket word has strictly positive sampling width.
Distinct definitions of this name: OAI/GroupTheory/PolycyclicRecognition/Algebra/WordExponentBounds.lean:15 (different declaration text). Qualify references as OAI.PolycyclicRecognition.bracketWordExponent_pos@path.
```
theorem bracketWordExponent_pos
    {I : Type*} [Fintype I] [DecidableEq I]
    (s : I → ℝ) (hs : ∀ i, 0 < s i) (w : FreeMagma I) :
    0 < bracketWordExponent s w := by
…
```
Mentions: OAI.PolycyclicRecognition.bracketWordExponent