FiniteAffineSelection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Canonical finite labels and separation from translated competitors

def OAI.PolycyclicRecognition.minimizingFiniteLabel line 15
Source documentation
Fix one minimizing label at every parameter value.
```
def minimizingFiniteLabel {L : Type*} [Fintype L] [Nonempty L] (cost : L → ℝ) : L :=
…
```
theorem OAI.PolycyclicRecognition.minimizingFiniteLabel_le line 18

theorem OAI.PolycyclicRecognition.minimizingFiniteLabel_tendsto_zero line 24

Source documentation

The canonical choices inherit any vanishing competitor bound.

theorem minimizingFiniteLabel_tendsto_zero
    {L : Type*} [Fintype L] [Nonempty L] (cost : ℕ → L → ℝ)
    (hnonneg : ∀ n a, 0 ≤ cost n a)
    (a : ℕ → L) (ha : Tendsto (fun n => cost n (a n)) atTop (𝓝 0)) :
    Tendsto (fun n => cost n (minimizingFiniteLabel (cost n))) atTop (𝓝 0) :=
…

Mentions: OAI.PolycyclicRecognition.minimizingFiniteLabel

theorem OAI.PolycyclicRecognition.linear_profile_distance_le_twice_affine line 33

Source documentation

Subtracting the value at the identity costs at most a factor of two in the uniform norm. This removes arbitrary offsets from a comparison.

theorem linear_profile_distance_le_twice_affine
    {Z W : Type*} [TopologicalSpace Z] [CompactSpace Z] [NormedAddCommGroup W]
    (A B : C(Z, W)) (z₀ : Z) (hA : A z₀ = 0) (hB : B z₀ = 0) (b c : W) :
    dist A B ≤ 2 * dist (A + ContinuousMap.const Z b) (B + ContinuousMap.const Z c) := by
…

theorem OAI.PolycyclicRecognition.exists_finite_affine_label_separation line 56

Source documentation

Finitely many distinct centered profiles have a uniform positive separation, even after arbitrary offsets are added.

theorem exists_finite_affine_label_separation
    {Z W L : Type*} [TopologicalSpace Z] [CompactSpace Z] [NormedAddCommGroup W]
    [Fintype L] [Nonempty L] (A : L → C(Z, W)) (hA : Function.Injective A)
    (z₀ : Z) (hzero : ∀ a, A a z₀ = 0) :
    ∃ ε : ℝ, 0 < ε ∧ ∀ a a' b b',
      dist (A a + ContinuousMap.const Z b) (A a' + ContinuousMap.const Z b') < ε → a = a' := by
…