OAI/Probability/SKFluctuations/PhysicalMomentOrder.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Physical Moment Order.

  1. theorem OAI.SKFluctuations.integral_power_root_mono_mul line 15
  2. theorem OAI.SKFluctuations.physicalNearRadiusIntegral_measurable line 33
  3. theorem OAI.SKFluctuations.physicalNearRadiusIntegral_bound line 48
  4. theorem OAI.SKFluctuations.physicalNearRadiusIntegral_raw line 65
  5. theorem OAI.SKFluctuations.physicalNear_mass_le_radius line 103
  6. theorem OAI.SKFluctuations.physicalNear_mass_raw line 137
  7. theorem OAI.SKFluctuations.Hierarchy.integral_power_root_sum_le_card line 173
  8. def OAI.SKFluctuations.physicalPairMassIntegral line 195
  9. theorem OAI.SKFluctuations.physicalPairMassIntegral_measurable line 201
  10. theorem OAI.SKFluctuations.physicalPairMassIntegral_nonneg line 211
  11. theorem OAI.SKFluctuations.physicalPairMassIntegral_le line 218
  12. theorem OAI.SKFluctuations.eventually_physical_pair_band_sum line 244
  13. def OAI.SKFluctuations.physicalSusceptibilityMassIntegral line 311
  14. theorem OAI.SKFluctuations.physicalSusceptibilityMassIntegral_le_array line 316
  15. theorem OAI.SKFluctuations.eventually_physical_susceptibility_band line 357
  16. def OAI.SKFluctuations.physicalWindowMass line 419
  17. def OAI.SKFluctuations.physicalWindowWeight line 422
  18. def OAI.SKFluctuations.physicalWindowCellMass line 426
  19. theorem OAI.SKFluctuations.physicalWindowWeight_nonneg line 430
  20. theorem OAI.SKFluctuations.physicalWindowWeight_normalized line 438
  21. theorem OAI.SKFluctuations.physicalWindowCellMass_nonneg line 445
  22. theorem OAI.SKFluctuations.physical_radius_window_energy line 453
  23. theorem OAI.SKFluctuations.physical_radius_window_cap line 476
  24. theorem OAI.SKFluctuations.radiusCellMeasure_real_univ line 499
  25. theorem OAI.SKFluctuations.physical_radius_window_mass line 506
  26. def OAI.SKFluctuations.dyadicLayerScale line 527
  27. theorem OAI.SKFluctuations.dyadicLayerScale_zero line 529
  28. theorem OAI.SKFluctuations.dyadicLayerScale_one line 530
  29. theorem OAI.SKFluctuations.dyadicLayerScale_monotone line 532
  30. theorem OAI.SKFluctuations.le_dyadicLayerScale line 537
  31. theorem OAI.SKFluctuations.dyadicLayerScale_pos line 540
  32. theorem OAI.SKFluctuations.dyadicRadiusNode_le_twice_scale line 543
  33. theorem OAI.SKFluctuations.dyadicRadiusNode_ge_scale line 553
  34. theorem OAI.SKFluctuations.physicalDyadicMass_scale_bound line 561