OAI/NumberTheory/Ostmann/Construction/WordTransferGuardFamily.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.wordGuardNumerators line 11
2. def OAI.Ostmann.wordGuardDenominators line 15
3. def OAI.Ostmann.wordGuardModuli line 19
4. def OAI.Ostmann.wordGuardPolynomials line 22
5. def OAI.Ostmann.wordGuardKeep line 27
6. theorem OAI.Ostmann.wordGuard_residue_iff line 31
7. theorem OAI.Ostmann.wordGuard_keep_iff line 38
8. theorem OAI.Ostmann.wordGuard_family_support line 56

   Source documentation

   The full branching support is exactly the residue-and-polynomial gate accepted by the one-sided estimate.

   theorem wordGuard_family_support {σ : Type*} {k : ℕ} (G : Fin k → WordTransferGuard σ)
       (a : σ → ℤ) (coord : σ) (z : ℤ) :
       (∀ i, (G i).ValidAt (Function.update a coord z)) ↔
         (∀ j, smallDivisionTest
           (MvPolynomial.eval₂ (RingHom.id ℤ) (Function.update a coord z) (wordGuardNumerators G j))
           (wordGuardDenominators G j) (wordGuardModuli G j)) ∧
         wordGuardKeep G (polynomialSupportCode (wordGuardPolynomials G a coord) (z : ℝ)) = true := by
   …

   Mentions: OAI.Ostmann.WordTransferGuard, OAI.Ostmann.smallDivisionTest, OAI.Ostmann.wordGuardNumerators, OAI.Ostmann.wordGuardDenominators, OAI.Ostmann.wordGuardModuli, OAI.Ostmann.wordGuardKeep, OAI.Ostmann.polynomialSupportCode, OAI.Ostmann.wordGuardPolynomials

9. theorem OAI.Ostmann.wordGuard_family_amplitude line 66
10. theorem OAI.Ostmann.wordGuard_family_degree line 76