OAI/Probability/SKFluctuations/ScalarSourceJet.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Scalar Source Jet.

  1. def OAI.SKFluctuations.Hierarchy.scalarSourceJet line 21
  2. theorem OAI.SKFluctuations.Hierarchy.scalarFeature_one_abs line 27
  3. theorem OAI.SKFluctuations.Hierarchy.scalarSourceJet_hasDerivAt line 31
  4. theorem OAI.SKFluctuations.Hierarchy.scalarSourceJet_bound line 54
  5. def OAI.SKFluctuations.Hierarchy.heatSteps line 68
  6. theorem OAI.SKFluctuations.Hierarchy.scalar_schedule_eq_hierarchy line 71
  7. theorem OAI.SKFluctuations.Hierarchy.OrderedSteps.lower line 94
  8. theorem OAI.SKFluctuations.Hierarchy.OrderedSteps.append_bound line 100
  9. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.grid_mass_bounds line 109
  10. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.grid_ordered line 131
  11. def OAI.SKFluctuations.Hierarchy.NonnegativeMassProfile.cappedApprox line 162
  12. theorem OAI.SKFluctuations.Hierarchy.NonnegativeMassProfile.cappedApprox_le_one line 167
  13. theorem OAI.SKFluctuations.Hierarchy.NonnegativeMassProfile.cappedApprox_error line 171
  14. theorem OAI.SKFluctuations.Hierarchy.scalar_capped_profile_error line 186
  15. theorem OAI.SKFluctuations.Hierarchy.scalar_capped_grid_error line 203
  16. theorem OAI.SKFluctuations.Hierarchy.scalar_capped_grid_tendstoUniformly line 223
  17. theorem OAI.SKFluctuations.Scalar.deriv_abs_le_secant line 245
  18. theorem OAI.SKFluctuations.Scalar.uniformCauchySeqOn_derivative line 269
  19. def OAI.SKFluctuations.Scalar.jetLimit line 302
  20. theorem OAI.SKFluctuations.Scalar.jet_uniformCauchy line 305
  21. theorem OAI.SKFluctuations.Scalar.jet_tendstoUniformly line 317
  22. theorem OAI.SKFluctuations.Scalar.jetLimit_hasDerivAt line 327
  23. theorem OAI.SKFluctuations.Scalar.jetLimit_bound line 336
  24. theorem OAI.SKFluctuations.Scalar.contDiff_of_derivative_chain line 353
  25. theorem OAI.SKFluctuations.Scalar.jetLimit_contDiff line 368
  26. theorem OAI.SKFluctuations.Scalar.jetLimit_iterated_deriv line 375
  27. def OAI.SKFluctuations.Hierarchy.scalarCappedJets line 392
  28. def OAI.SKFluctuations.Hierarchy.scalarProfileJet line 396
  29. theorem OAI.SKFluctuations.Hierarchy.scalarCappedJets_ordered line 399
  30. theorem OAI.SKFluctuations.Hierarchy.scalarCappedJets_hasDerivAt line 405
  31. theorem OAI.SKFluctuations.Hierarchy.scalarCappedJets_bound line 410
  32. theorem OAI.SKFluctuations.Hierarchy.scalarCappedJets_zero_tendsto line 415
  33. theorem OAI.SKFluctuations.Hierarchy.scalarCappedJets_zero_cauchy line 424
  34. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_tendstoUniformly line 429
  35. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_zero line 435
  36. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_hasDerivAt line 441
  37. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_bound line 447
  38. theorem OAI.SKFluctuations.Hierarchy.scalarProfile_contDiff line 456
  39. theorem OAI.SKFluctuations.Hierarchy.scalarProfile_iterated_deriv line 462
  40. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_bddSmooth line 476
  41. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_lipschitz line 484
  42. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_line line 493
  43. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_coord line 503
  44. def OAI.SKFluctuations.Hierarchy.scalarProfileHeatJet line 514
  45. theorem OAI.SKFluctuations.Hierarchy.scalarProfileHeatJet_F line 540
  46. theorem OAI.SKFluctuations.Hierarchy.HeatJet.capped_profile_error line 557
  47. theorem OAI.SKFluctuations.Hierarchy.HeatJet.capped_grid_error line 574
  48. theorem OAI.SKFluctuations.Hierarchy.HeatJet.capped_grid_tendsto line 593
  49. theorem OAI.SKFluctuations.Hierarchy.scalarProfileHeatJet_G_bound line 613
  50. theorem OAI.SKFluctuations.Hierarchy.scalarProfile_midpoint line 621
  51. theorem OAI.SKFluctuations.GaussianCalculus.ExpBounded.const line 654
  52. theorem OAI.SKFluctuations.GaussianCalculus.ExpBounded.id line 658
  53. theorem OAI.SKFluctuations.GaussianCalculus.ExpBounded.neg line 661
  54. theorem OAI.SKFluctuations.GaussianCalculus.ExpBounded.add line 665
  55. theorem OAI.SKFluctuations.GaussianCalculus.ExpBounded.sub line 677
  56. theorem OAI.SKFluctuations.GaussianCalculus.ExpBounded.mul line 680
  57. theorem OAI.SKFluctuations.GaussianCalculus.ExpBounded.const_mul line 691
  58. theorem OAI.SKFluctuations.GaussianCalculus.ExpBounded.pow line 694
  59. theorem OAI.SKFluctuations.GaussianCalculus.ExpBounded.integrable line 700
  60. theorem OAI.SKFluctuations.GaussianCalculus.ExpBounded.of_bddSmooth line 704