OAI/Probability/SKFluctuations/FilledSquare.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Filled Square.

  1. def OAI.SKFluctuations.Hierarchy.HeatJet.filledSquare line 21
  2. def OAI.SKFluctuations.Hierarchy.HeatJet.filledEnergy line 25
  3. theorem OAI.SKFluctuations.Hierarchy.HeatJet.hasDerivAt_filledSquare line 30
  4. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.continuousEnergy line 58
  5. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.boundedEnergy line 61
  6. theorem OAI.SKFluctuations.Hierarchy.HeatJet.continuous_filledSquare line 67
  7. theorem OAI.SKFluctuations.Hierarchy.HeatJet.continuous_filledEnergy line 75
  8. theorem OAI.SKFluctuations.Hierarchy.HeatJet.filledEnergy_nonneg line 83
  9. theorem OAI.SKFluctuations.Hierarchy.HeatJet.filledSquare_zero line 89
  10. theorem OAI.SKFluctuations.Hierarchy.HeatJet.filledSquare_terminal line 95
  11. theorem OAI.SKFluctuations.Hierarchy.HeatJet.variance_eq_integral_energy line 104
  12. theorem OAI.SKFluctuations.Hierarchy.clockTest_zero_potential line 122
  13. theorem OAI.SKFluctuations.Hierarchy.clockTest_zero_mass line 126
  14. theorem OAI.SKFluctuations.Hierarchy.clockContinuation_zero_potential line 130
  15. theorem OAI.SKFluctuations.Hierarchy.clockRoot_zero line 135
  16. def OAI.SKFluctuations.Hierarchy.HeatJet.erasePotential line 140
  17. def OAI.SKFluctuations.Hierarchy.HeatJet.rootFilledSquare line 159
  18. def OAI.SKFluctuations.Hierarchy.HeatJet.rootFilledEnergy line 161
  19. theorem OAI.SKFluctuations.Hierarchy.HeatJet.erased_filledSquare line 164
  20. theorem OAI.SKFluctuations.Hierarchy.HeatJet.erased_filledEnergy line 172
  21. theorem OAI.SKFluctuations.Hierarchy.HeatJet.hasDerivAt_rootFilledSquare line 182
  22. theorem OAI.SKFluctuations.Hierarchy.HeatJet.root_variance_eq_integral_energy line 190
  23. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.affine line 204
  24. def OAI.SKFluctuations.Hierarchy.HeatJet.ofTest line 219
  25. def OAI.SKFluctuations.Hierarchy.gaussianFeatureJet line 249
  26. theorem OAI.SKFluctuations.Hierarchy.gaussianFeatureJet_F line 269
  27. theorem OAI.SKFluctuations.Hierarchy.gaussianFeatureJet_A line 274
  28. theorem OAI.SKFluctuations.Hierarchy.gaussianFeatureJet_A₁ line 282
  29. def OAI.SKFluctuations.Hierarchy.replicaFeatureJet line 301
  30. theorem OAI.SKFluctuations.Hierarchy.replicaFeatureJet_F line 309
  31. theorem OAI.SKFluctuations.Hierarchy.replicaFeatureJet_A line 315
  32. theorem OAI.SKFluctuations.Hierarchy.replicaFeatureJet_A₁ line 321
  33. theorem OAI.SKFluctuations.Hierarchy.replicaFeatureJet_A₂ line 333
  34. def OAI.SKFluctuations.Hierarchy.ReplicaTree.powerTrace line 350
  35. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.powerTrace_smooth line 355
  36. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.powerTrace_eq_testedHeatTrace line 362
  37. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.powerTrace_one_eq_potentialHeatTrace line 376
  38. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.hasDerivWithinAt_linearClockTest line 392
  39. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.powerJet_two_abs_le line 420
  40. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.powerTrace_abs_le line 435
  41. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.clock_abs_le line 446
  42. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.clock_powerTrace_abs_le line 456
  43. def OAI.SKFluctuations.Hierarchy.ReplicaTree.clockResponse line 469
  44. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.clockResponse_abs_le line 476
  45. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.clock_lipschitz line 497
  46. structure OAI.SKFluctuations.Hierarchy.ParametricTest line 518
  47. theorem OAI.SKFluctuations.Hierarchy.ParametricTest.smooth0 line 526
  48. theorem OAI.SKFluctuations.Hierarchy.ParametricTest.response_smooth0 line 530
  49. theorem OAI.SKFluctuations.Hierarchy.ParametricRegular.response_smooth0 line 534
  50. theorem OAI.SKFluctuations.Hierarchy.ParametricTest.mul line 539
  51. def OAI.SKFluctuations.Hierarchy.tiltedResponse line 561
  52. theorem OAI.SKFluctuations.Hierarchy.ParametricTest.step line 566