OAI/GroupTheory/PolycyclicRecognition/Analysis/ConeSamplingTemplate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_cone_sampling_template line 16

   Source documentation

   A fixed positive polar radius works for every sufficiently small chart enlargement. The translated template lies in the scaled interior of the actual finite weight polytope.

   theorem exists_cone_sampling_template
       {W I : Type*} [NormedAddCommGroup W] [InnerProductSpace ℝ W]
       [FiniteDimensional ℝ W] [Fintype I]
       (α : I → W →L[ℝ] ℝ) (hne : ∀ i, α i ≠ 0)
       (i₀ : I) (C : ProperCone ℝ (W →L[ℝ] ℝ)) (hC : α i₀ ∈ C)
       {c c' : ℝ} (hc : 0 ≤ c) (hcc : c < c') :
       ∃ (p : W) (ε₀ δ₀ : ℝ), α i₀ p = ‖α i₀‖ ∧
         0 < ε₀ ∧ 0 < δ₀ ∧
         IsCompact ((fun z : W => ε₀ • z) '' conePolarTemplate C) ∧
         ∀ δ : ℝ, 0 < δ → δ ≤ δ₀ →
           (fun z : W => (1 - c' * δ) • p + ε₀ • z) '' conePolarTemplate C ⊆
             (fun y : W => (1 - c * δ) • y) '' interior (weightSamplingPolytope α) := by
   …

   Mentions: OAI.PolycyclicRecognition.conePolarTemplate, OAI.PolycyclicRecognition.weightSamplingPolytope