OAI/NumberTheory/Ostmann/Arithmetic/FrozenMovingSamples.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingSlotValues_congr line 10
2. theorem OAI.Ostmann.movingCompensationValues_congr line 24
3. theorem OAI.Ostmann.MovingSampleSlots.values_eq_of_levels line 40

   Source documentation

   All internal samples have lower tier than the current bulk. This proves equality of the complete sampled tree, including its shared child samples.

   theorem MovingSampleSlots.values_eq_of_levels {σ : Type*} (tier : σ → ℕ)
       (v w : σ → ℕ) (k : ℕ) (heq : ∀ i, tier i < k → v i = w i)
       {n : ℕ} (samples : MovingSampleSlots σ n) (hn : n ≤ k)
       (hlevels : samples.Levels tier) : samples.values v = samples.values w := by
   …

   Mentions: OAI.Ostmann.MovingSampleSlots

4. theorem OAI.Ostmann.frozenMoving_nonbulk_values line 60

   Source documentation

   Replacing precisely the selected bulk coordinates preserves both sources of nonbulk data used to construct the field diagram.

   theorem frozenMoving_nonbulk_values {σ J : Type*} (tier : σ → ℕ)
       (base value : σ → ℕ) (e : J ↪ σ) (n : ℕ)
       (he : ∀ j, n ≤ tier (e j))
       (hv : ∀ i ∉ Set.range e, value i = base i)
       (small : TreeLeafTuple (List σ) n) (samples : MovingSampleSlots σ n)
       (hsmall : ∀ i ∈ flattenMovingSlots n small, i ∉ Set.range e)
       (hsamples : samples.Levels tier) :
       movingSlotValues value n small = movingSlotValues base n small ∧
         samples.values value = samples.values base := by
   …

   Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.movingSlotValues