OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteSignOrder.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.positive_signs_eq_of_ordered line 15

   Source documentation

   A finite set of signs cannot change when every positive sign can only disappear and their total count stays constant.

   theorem positive_signs_eq_of_ordered
       {I : Type*} [Fintype I] (q : I → ℝ → ℝ) (τ : I → ℝ)
       {s t : ℝ} (hst : s ≤ t)
       (hs : ∀ i, q i s ≠ 0 ∧ (s ≤ τ i → 0 ≤ q i s) ∧ (τ i < s → q i s ≤ 0))
       (ht : ∀ i, q i t ≠ 0 ∧ (t ≤ τ i → 0 ≤ q i t) ∧ (τ i < t → q i t ≤ 0))
       (hcard : (Finset.univ.filter (fun i => 0 < q i s)).card =
         (Finset.univ.filter (fun i => 0 < q i t)).card) :
       ∀ i, (0 < q i s ↔ 0 < q i t) := by
   …

2. theorem OAI.PolycyclicRecognition.exists_constant_positive_signs line 42

   Source documentation

   The almost-everywhere version needed for the scalar derivatives of a profile. No monotonicity of the label itself is assumed.

   theorem exists_constant_positive_signs
       {I : Type*} [Fintype I] (q : I → ℝ → ℝ) (τ : I → ℝ)
       {a b : ℝ} (n : ℕ)
       (hnonzero : ∀ i, ∀ᵐ t ∂volume.restrict (Ioc a b), q i t ≠ 0)
       (hleft : ∀ i, ∀ᵐ t ∂volume.restrict (Ioc a (τ i)), 0 ≤ q i t)
       (hright : ∀ i, ∀ᵐ t ∂volume.restrict (Ioc (τ i) b), q i t ≤ 0)
       (hcard : ∀ᵐ t ∂volume.restrict (Ioc a b),
         (Finset.univ.filter (fun i => 0 < q i t)).card = n) :
       ∃ S : Finset I, ∀ᵐ t ∂volume.restrict (Ioc a b),
         ∀ i, (0 < q i t ↔ i ∈ S) := by
   …