OAI/MathematicalPhysics/CriticalSK/BlockEnergy.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.sum_consecutive_blocks line 28
  2. def OAI.CriticalSK.blockIndices line 36
  3. lemma OAI.CriticalSK.block_index_injective line 39
  4. lemma OAI.CriticalSK.blockIndices_sum line 52
  5. lemma OAI.CriticalSK.blockIndices_lower line 57
  6. lemma OAI.CriticalSK.sum_supported_le line 63
  7. lemma OAI.CriticalSK.supported_mass line 79
  8. lemma OAI.CriticalSK.supported_shift_mass line 84
  9. lemma OAI.CriticalSK.supported_energy_tail line 93
  10. lemma OAI.CriticalSK.supported_energy_gradient line 106
  11. lemma OAI.CriticalSK.supported_shift_energy_gradient line 121
  12. lemma OAI.CriticalSK.many_block_prefix_abs_bound line 131
  13. lemma OAI.CriticalSK.supported_shift_energy_tail line 153
  14. lemma OAI.CriticalSK.localized_product_mass line 167
  15. lemma OAI.CriticalSK.localized_square_variation line 179
  16. lemma OAI.CriticalSK.localized_product_variation line 196
  17. lemma OAI.CriticalSK.sum_covered_by_shells line 214
  18. lemma OAI.CriticalSK.sum_range_eq_of_supported line 228
  19. lemma OAI.CriticalSK.shell_indices_mass line 236
  20. lemma OAI.CriticalSK.half_pow_le_three_quarters_sq line 269
  21. lemma OAI.CriticalSK.sqrt_shell_energy_bound line 274
  22. lemma OAI.CriticalSK.shell_square_mass_variation line 283
  23. lemma OAI.CriticalSK.shell_product_mass_variation line 303
  24. lemma OAI.CriticalSK.weighted_geometric_three_quarters line 321
  25. lemma OAI.CriticalSK.shifted_weighted_geometric line 332
  26. lemma OAI.CriticalSK.weighted_multiscale_prefix line 343
  27. lemma OAI.CriticalSK.square_multiscale_prefix line 395
  28. lemma OAI.CriticalSK.product_multiscale_prefix line 411
  29. lemma OAI.CriticalSK.blockThreshold_linear_bound line 427
  30. lemma OAI.CriticalSK.blockThreshold_length_bound line 447