OAI/Combinatorics/SumProduct/Alignment/MicrocellHarmonic01.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RoughFaceShift.raw_conditional_face_uniform line 23
  2. def OAI.HarmonicExposure.rawTailFiber line 93
  3. def OAI.HarmonicExposure.literalFiberMass line 99
  4. lemma OAI.HarmonicExposure.rawTail_cast_mem line 106
  5. lemma OAI.HarmonicExposure.times_nonneg line 117
  6. lemma OAI.HarmonicExposure.times_nat_mem line 124
  7. theorem OAI.HarmonicExposure.literal_mass_eq line 154
  8. def OAI.MicrocellHarmonic.weight line 197
  9. def OAI.MicrocellHarmonic.uniform line 199
  10. lemma OAI.MicrocellHarmonic.total_pos line 201
  11. lemma OAI.MicrocellHarmonic.sum_weight line 204
  12. theorem OAI.MicrocellHarmonic.normalized_error line 210
  13. theorem OAI.MicrocellHarmonic.l1_error line 231
  14. theorem OAI.MicrocellHarmonic.test_error line 241
  15. lemma OAI.MicrocellHarmonic.reciprocal_oscillation line 254
  16. theorem OAI.MicrocellHarmonic.harmonic_test_error line 269