OAI/NumberTheory/Ostmann/Construction/WordTransferGuardPolynomial.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.WordTransferGuard.residueAt line 11
2. def OAI.Ostmann.WordTransferGuard.frequencyBounds line 17
3. def OAI.Ostmann.WordTransferGuard.polynomials line 20
4. theorem OAI.Ostmann.WordTransferGuard.gap_iff line 27
5. theorem OAI.Ostmann.WordTransferGuard.validAt_polynomials line 47

   Source documentation

   Strict product gaps are closed polynomial inequalities because the residue tests already enforce the exact integral word values.

   theorem WordTransferGuard.validAt_polynomials {σ : Type*}
       (g : WordTransferGuard σ) (a : σ → ℤ) (coord : σ) (z : ℤ) :
       g.ValidAt (Function.update a coord z) ↔
         g.residueAt (Function.update a coord z) ∧ g.frequencyBounds ∧
           ∀ j, 0 ≤ (g.polynomials a coord j).eval (z : ℝ) := by
   …

   Mentions: OAI.Ostmann.WordTransferGuard

6. theorem OAI.Ostmann.WordTransferGuard.polynomials_degree line 68

   Source documentation

   Each node contributes three inequalities of derived polynomial degree.

   theorem WordTransferGuard.polynomials_degree {σ : Type*}
       (g : WordTransferGuard σ) (a : σ → ℤ) (coord : σ) :
       ∀ j, (g.polynomials a coord j).natDegree ≤ max g.pivot.cost g.rightProduct.cost := by
   …

   Mentions: OAI.Ostmann.WordTransferGuard