OAI/NumberTheory/Ostmann/Arithmetic/MovingTemplateTransferSupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.indexed_coprime_of_list line 11
2. theorem OAI.Ostmann.movingTemplateCoefficient_transfer_support line 24

   Source documentation

   The complete current Fourier slots inherit pairwise and outside coprimality directly from the support of their coefficient.

   theorem movingTemplateCoefficient_transfer_support {σ : Type} [Fintype σ]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n r m : ℕ) (s : ℤ)
       (y : MovingRegularSlot n r m → σ) (q : Bool → ℕ)
       (h : movingTemplateCoefficient value outside μ childBound pivotBound V F φ G
         n r m s y (q true) (q false) ≠ 0) :
       Pairwise (fun i j => (Sum.elim q (value ∘ y) i).Coprime (Sum.elim q (value ∘ y) j)) ∧
         ∀ i, outside.prod.Coprime (Sum.elim q (value ∘ y) i) := by
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingTemplateCoefficient

3. theorem OAI.Ostmann.movingTemplateCoefficient_restored_support line 57

   Source documentation

   Restrict the full support to the two pieces of a restored child. This supplies the exact support fields of the giant transfer.

   theorem movingTemplateCoefficient_restored_support {σ : Type} [Fintype σ]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n r m : ℕ) (s : ℤ)
       (u : TreeLeafIndex n × Fin 4 → σ) (y : MovingRegularSlot n r m → σ)
       (p X : ℕ)
       (h : movingTemplateCoefficient value outside μ childBound pivotBound V F φ G
         n (4 + r) m s (movingRestoreSample n r m u y) p X ≠ 0) :
       let Q := Sum.elim (fun _ : Unit => p) (value ∘ u)
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingTemplateCoefficient, OAI.Ostmann.movingRestoreSample