OAI/Combinatorics/SumProduct/Alignment/AllLevel09.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TwoScaleInvariance.integral_eq line 37
  2. theorem OAI.TwoScaleInvariance.map_eq line 66
  3. theorem OAI.TwoScaleInvariance.range_preservation line 80
  4. def OAI.AllLevelFactorization.Factorization.ResidueCover.marginalBoxAverage line 146
  5. def OAI.AllLevelFactorization.Factorization.ResidueCover.marginalCubeHaar line 150
  6. lemma OAI.AllLevelFactorization.Factorization.ResidueCover.marginal_local_law line 155
  7. theorem OAI.AllLevelFactorization.Factorization.ResidueCover.marginal_haar_invariant line 196
  8. instance OAI.AllLevelFactorization.Factorization.ResidueCover.haar_fullSupport line 227
  9. def OAI.AllLevelFactorization.Factorization.ResidueCover.cubePhysical line 236
  10. lemma OAI.AllLevelFactorization.Factorization.ResidueCover.cubePhysical_mk line 246
  11. theorem OAI.AllLevelFactorization.Factorization.ResidueCover.physical_cube_image_preserved line 260