OAI/Analysis/StrictMeans/DiagonalIndex.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.Grid.lineIndex_mul_pos line 11
  2. lemma OAI.StrictInverseFirstPower.Grid.signed_square_index line 15
  3. def OAI.StrictInverseFirstPower.Grid.signedVertex line 25
  4. lemma OAI.StrictInverseFirstPower.Grid.signed_diagonal_index line 28
  5. lemma OAI.StrictInverseFirstPower.Grid.diagonal_sample line 44
  6. lemma OAI.StrictInverseFirstPower.Grid.nearest_integer_bound line 55
  7. lemma OAI.StrictInverseFirstPower.Grid.signedVertex_close line 63
  8. lemma OAI.StrictInverseFirstPower.Grid.diagonal_local_sum line 85