OAI/Analysis/PeriodicLattice/Main.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform force compilers and the complete periodic lattice memory theorem.

  1. theorem OAI.PeriodicLattice.EffectiveFields.mixedWord_recursive line 21
  2. theorem OAI.PeriodicLattice.EffectiveFields.uniformlyEffective_of_certificate line 31
  3. theorem OAI.PeriodicLattice.periodic_lattice_memory line 83