OAI/NumberTheory/Ostmann/Arithmetic/CompensatedPairSupport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.pairArithmeticData line 11
2. theorem OAI.Ostmann.pairArithmeticData_test line 17
3. theorem OAI.Ostmann.sequentialSupport_and line 23
4. theorem OAI.Ostmann.arithmeticLeafSupport_pair line 35
5. def OAI.Ostmann.compensatedPairData line 44
6. theorem OAI.Ostmann.compensatedPairData_frequencies line 54
7. theorem OAI.Ostmann.compensatedPairData_actual_support line 79

   Source documentation

   Both histories use one bulk residue tuple; no history validity is used as a conditioning event.

   theorem compensatedPairData_actual_support (n R k : ℕ) [NeZero (R ^ (k + 2))]
       (D E : PivotDependencyScheme (2 ^ n - 1)) (U V : Fin (2 ^ n - 1) → ℤ)
       (hU : ∀ i, IsCoprime (U i) (R : ℤ)) (hV : ∀ i, IsCoprime (V i) (R : ℤ))
       (hdepthD : ∀ i, D.depth i ≤ k) (hdepthE : ∀ i, E.depth i ≤ k)
       (hD : ∀ i, (D.frequencies i).root ≠ 0) (hE : ∀ i, (E.frequencies i).root ≠ 0)
       (hDR : ∀ i, (D.frequencies i).root.natAbs ∣ R)
       (hER : ∀ i, (E.frequencies i).root.natAbs ∣ R)
       (a b : SampledPivotHistory n (R ^ (k + 2)))
       (ha : a.compensatedValid D U) (hb : b.compensatedValid E V) (hab : a.residue = b.residue) :
       arithmeticLeafSupport n (compensatedPairData n R k D E U V hD hE hDR hER) a.residue = 1 := by
   …

   Mentions: OAI.Ostmann.PivotDependencyScheme, OAI.Ostmann.SampledPivotHistory, OAI.Ostmann.arithmeticLeafSupport, OAI.Ostmann.compensatedPairData