OAI/NumberTheory/Ostmann/Arithmetic/MovingSquareSupport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.MovingSlotData.CompensationPrimeData line 10
2. def OAI.Ostmann.MovingSlotData.CompensationDistinct line 20

   Source documentation

   Equality patterns may identify samples at different nodes; only the entries made together in one compensation vector have to be distinct.

   def MovingSlotData.CompensationDistinct {σ : Type*} (value : σ → ℕ) :
       {n : ℕ} → MovingSlotData σ n → Prop
     | _, .leaf _ _ => True
     | _, .node _ _ _ U left right =>
         (U.map value).Pairwise Nat.Coprime ∧
         left.CompensationDistinct value ∧ right.CompensationDistinct value

   Mentions: OAI.Ostmann.MovingSlotData

3. def OAI.Ostmann.MovingSampleSlots.DistinctCompensations line 27
4. theorem OAI.Ostmann.buildMovingSlotData_compensation_distinct line 34
5. theorem OAI.Ostmann.MovingSlotData.compensationPrimeData_of_ranges line 45

   Source documentation

   The manuscript's size separation proves the frequency-prime coprimality required by the square tests. It is not an additional analytic input.

   theorem MovingSlotData.compensationPrimeData_of_ranges {σ : Type*} (value : σ → ℕ)
       (hprime : ∀ i, (value i).Prime) (V : ℕ) (hlarge : ∀ i, V < value i)
       {n : ℕ} (T : MovingSlotData σ n)
       (hf : T.Frequencies (· ≠ 0)) (hV : T.Frequencies (fun s => s.natAbs ≤ V))
       (hdistinct : T.CompensationDistinct value) : T.CompensationPrimeData value := by
   …

   Mentions: OAI.Ostmann.MovingSlotData

6. def OAI.Ostmann.MovingSlotData.PrimeSquareTests line 64

   Source documentation

   The numerator at every node is tested before division by the node's frequency or by its compensation product.

   def MovingSlotData.PrimeSquareTests {σ : Type*} (value : σ → ℕ) :
       {n : ℕ} → MovingSlotData σ n → ℕ → ℕ → Prop
     | _, .leaf _ _, _, _ => True
     | _, .node s CL CR U left right, XL, XR =>
         let p := (MovingSlotData.step s CL CR U left right false).naturalPivot value XL XR
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingSlotData.step

7. theorem OAI.Ostmann.MovingSlotData.newCompensationUnits_iff_squareTests line 74
8. theorem OAI.Ostmann.MovingSlotData.fullPairwise_iff_squareTests line 101

   Source documentation

   An exact reduction of all pairwise slot tests to the top support and the explicit numerator exclusions modulo b², for the original integral tree.

   theorem MovingSlotData.fullPairwise_iff_squareTests {σ : Type*} (value : σ → ℕ)
       {n : ℕ} (T : MovingSlotData σ n) (hcoh : T.RegularCoherent)
       (hprime : T.CompensationPrimeData value) (XL XR : ℕ)
       (hI : T.Integral value XL XR) (hfreq : T.CrossFrequencyUnits value XL XR) :
       T.FullPairwise value XL XR ↔ T.CurrentPairwise value XL XR ∧ T.PrimeSquareTests value XL XR := by
   …

   Mentions: OAI.Ostmann.MovingSlotData