OAI/Probability/SKFluctuations/ActualPairCut.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Actual Pair Cut.

  1. def OAI.SKFluctuations.Hierarchy.actualPairCut line 22
  2. theorem OAI.SKFluctuations.Hierarchy.actualPairCut_measurable_joint line 29
  3. theorem OAI.SKFluctuations.Hierarchy.actualPairCut_measurable line 39
  4. theorem OAI.SKFluctuations.Hierarchy.bddSmooth0_tensor line 44
  5. theorem OAI.SKFluctuations.Hierarchy.integrable_actualPairCut_tensor line 56
  6. theorem OAI.SKFluctuations.Hierarchy.integral_actualPairCut_tensor line 68
  7. theorem OAI.SKFluctuations.GaussianCalculus.lipschitz_of_sourceJet line 121
  8. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivAt_integral_tested_scaledSource line 147
  9. def OAI.SKFluctuations.Hierarchy.HeatJet.one line 233
  10. def OAI.SKFluctuations.Hierarchy.HeatJet.testedInsertion line 254
  11. theorem OAI.SKFluctuations.Hierarchy.HeatJet.smooth_testedInsertion line 258
  12. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivAt_integral_diagonal_tested_heat line 271
  13. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivAt_diagonal_heat_test line 322
  14. def OAI.SKFluctuations.Hierarchy.HeatJet.potentialInsertion line 360
  15. theorem OAI.SKFluctuations.Hierarchy.HeatJet.smooth_potentialInsertion line 363
  16. def OAI.SKFluctuations.Hierarchy.HeatJet.signedVarianceRate line 369
  17. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_signed_variance_test line 376
  18. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.continuous_testedInsertion line 429
  19. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.bounded_testedInsertion line 435
  20. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.continuous_potentialInsertion line 443
  21. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.bounded_potentialInsertion line 448
  22. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_dynamic_varianceTest line 457