OAI/Analysis/NodalLength/Lattice.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SharpNodal.Grid.Point line 208
  2. def OAI.SharpNodal.Grid.box line 210
  3. lemma OAI.SharpNodal.Grid.mem_box line 212
  4. lemma OAI.SharpNodal.Grid.card_box line 215
  5. lemma OAI.SharpNodal.Grid.box_mono line 218
  6. def OAI.SharpNodal.Grid.square line 224
  7. lemma OAI.SharpNodal.Grid.mem_square line 227
  8. lemma OAI.SharpNodal.Grid.card_square line 230
  9. lemma OAI.SharpNodal.Grid.mem_square_div line 237
  10. lemma OAI.SharpNodal.Grid.square_disjoint line 246
  11. def OAI.SharpNodal.Grid.neighborhood line 253
  12. lemma OAI.SharpNodal.Grid.mem_neighborhood line 256
  13. lemma OAI.SharpNodal.Grid.card_neighborhood line 260
  14. lemma OAI.SharpNodal.Grid.square_subset_neighborhood line 269
  15. lemma OAI.SharpNodal.Profiles.UnitWave.growth_nonneg line 279
  16. lemma OAI.SharpNodal.Profiles.UnitWave.growth_change line 282
  17. lemma OAI.SharpNodal.Profiles.GridChild.same_growth line 298
  18. theorem OAI.SharpNodal.Profiles.entry_growth_bound line 303
  19. theorem OAI.SharpNodal.Grid.finite_witness_packing line 353