MovingChildListSupport.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The restored child lists supply the support used by the transfer

theorem OAI.Ostmann.movingFrequencyCoefficient_child_pairwise line 11

Source documentation

Restoring compensation does not change its order-free current support.

theorem movingFrequencyCoefficient_child_pairwise {σ : Type} [Fintype σ]
    (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
    (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
    (φ : ℝ → ℝ) (G : ℕ → ℝ) (n : ℕ) (s : ℤ)
    (u small bulk : TreeLeafTuple (List σ) n) (p X : ℕ)
    (h : movingFrequencyCoefficient value outside μ childBound pivotBound V F φ G n s
      (appendMovingSlotLeaves n u small) bulk p X ≠ 0) :
    (p :: X :: ((flattenMovingSlots n u).map value ++
      ((flattenMovingSlots n small ++ flattenMovingSlots n bulk).map value ++ outside))).Pairwise Nat.Coprime := by
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingFrequencyCoefficient, OAI.Ostmann.appendMovingSlotLeaves, OAI.Ostmann.flattenMovingSlots

theorem OAI.Ostmann.restored_child_product_support line 30

Source documentation

A restored child is disjoint from the inserted giant and its shared compensation vector. These are precisely the product units needed in the integer substitution.

theorem restored_child_product_support (u small outside : List ℕ) (p X : ℕ)
    (h : (p :: X :: (u ++ (small ++ outside))).Pairwise Nat.Coprime) :
    (X :: (small ++ outside)).Pairwise Nat.Coprime ∧
      (X * small.prod).Coprime (p * u.prod) := by
…

theorem OAI.Ostmann.movingFrequencyCoefficient_child_products line 56

Source documentation

The inherited product in a nonzero child is coprime to the composite pivot, even when the newly inserted giant is only an integer.

theorem movingFrequencyCoefficient_child_products {σ : Type} [Fintype σ]
    (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
    (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
    (φ : ℝ → ℝ) (G : ℕ → ℝ) (n : ℕ) (s : ℤ)
    (u small bulk : TreeLeafTuple (List σ) n) (p X : ℕ)
    (h : movingFrequencyCoefficient value outside μ childBound pivotBound V F φ G n s
      (appendMovingSlotLeaves n u small) bulk p X ≠ 0) :
    (X :: (((flattenMovingSlots n small ++ flattenMovingSlots n bulk).map value) ++ outside)).Pairwise Nat.Coprime ∧
      (X * MovingSlotReversal.naturalProduct value
        (flattenMovingSlots n small ++ flattenMovingSlots n bulk)).Coprime
        (p * MovingSlotReversal.naturalProduct value (flattenMovingSlots n u)) := by
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingFrequencyCoefficient, OAI.Ostmann.appendMovingSlotLeaves, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.MovingSlotReversal.naturalProduct