OAI/Probability/ClassicalON/LatticeModes.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClassicalON.latticeMode line 11
  2. theorem OAI.ClassicalON.groupedPoint_abs_bound line 15
  3. theorem OAI.ClassicalON.groupedWave_axis line 28
  4. theorem OAI.ClassicalON.groupedWave_axis_sine line 33
  5. theorem OAI.ClassicalON.groupedWave_multiplier_bound line 45
  6. theorem OAI.ClassicalON.latticeMode_norm_bound line 66
  7. def OAI.ClassicalON.LatticeGraph.modeGradient line 74
  8. def OAI.ClassicalON.LatticeGraph.scaledModeGradient line 77
  9. theorem OAI.ClassicalON.LatticeGraph.scaledModeGradient_formula line 80