OAI/Combinatorics/SumProduct/Alignment/ProductExposure02.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RoughFaceShift.source_raw_joint_face_uniform line 23
  2. structure OAI.ProductExposureLabels.Label line 88
  3. def OAI.ProductExposureLabels.Label.scales line 94
  4. def OAI.ProductExposureLabels.Label.width line 96
  5. def OAI.ProductExposureLabels.Label.left line 98
  6. def OAI.ProductExposureLabels.expose line 100
  7. def OAI.ProductExposureLabels.rawDomain line 106
  8. lemma OAI.ProductExposureLabels.Label.ext line 110
  9. lemma OAI.ProductExposureLabels.dyadic_iff line 114
  10. lemma OAI.ProductExposureLabels.residue_iff line 127
  11. lemma OAI.ProductExposureLabels.floor_bin_iff line 132
  12. lemma OAI.ProductExposureLabels.Label.width_pos line 137
  13. lemma OAI.ProductExposureLabels.expose_eq_iff line 142
  14. theorem OAI.ProductExposureLabels.fiber_eq line 182
  15. def OAI.ProductExposureCutoff.cutoff line 217
  16. lemma OAI.ProductExposureCutoff.mass_mono_interval line 219
  17. lemma OAI.ProductExposureCutoff.many_dyadic_lower line 223
  18. lemma OAI.ProductExposureCutoff.dyadic_upper_simple line 237
  19. lemma OAI.ProductExposureCutoff.many_dyadic_upper line 250
  20. lemma OAI.ProductExposureCutoff.cutoff_mass_bound line 264
  21. theorem OAI.ProductExposureCutoff.raw_cutoff_bound line 324
  22. theorem OAI.ProductExposureCutoff.raw_cutoff_decay line 345