OAI/Probability/SKFluctuations/TransformedDensityShape.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Transformed Density Shape.

  1. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.potential_eq line 21
  2. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.potential_hasDerivAt line 31
  3. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.potential_deriv line 42
  4. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.potential_second_hasDerivAt line 46
  5. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.potential_second line 51
  6. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.potential_third_hasDerivAt line 55
  7. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.potential_third line 61
  8. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.potential_even line 65
  9. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.potential_gradient_zero line 68
  10. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.potential_curvature_lower line 79
  11. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.potential_shape line 84
  12. def OAI.SKFluctuations.Hierarchy.ResidualJet.constant line 108
  13. theorem OAI.SKFluctuations.Hierarchy.ResidualJet.constant_cone line 116
  14. def OAI.SKFluctuations.Hierarchy.GaussianResidual.initial line 119
  15. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.density_initial line 122
  16. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.density_heat_zero line 127
  17. inductive OAI.SKFluctuations.Hierarchy.DensityStep line 138
  18. def OAI.SKFluctuations.Hierarchy.DensityStep.apply line 143
  19. theorem OAI.SKFluctuations.Hierarchy.DensityStep.cone line 148
  20. def OAI.SKFluctuations.Hierarchy.finiteTransformedResidual line 154
  21. theorem OAI.SKFluctuations.Hierarchy.DensityStep.fold_cone line 157
  22. theorem OAI.SKFluctuations.Hierarchy.finiteTransformedResidual_cone line 164
  23. theorem OAI.SKFluctuations.Hierarchy.finiteTransformedDensity_shape line 170
  24. theorem OAI.SKFluctuations.Hierarchy.exp_mul_shiftedContinuation_all line 186
  25. theorem OAI.SKFluctuations.Hierarchy.realGaussianKernel_exp_shift line 194
  26. def OAI.SKFluctuations.Hierarchy.GaussianResidual.plantedDensity line 210
  27. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.plantedDensity_pos line 213
  28. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.plantedDensity_integrable line 216
  29. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.plantedDensity_heat_integral line 219
  30. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.plantedDensity_continuation_integrable line 241
  31. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.plantedDensity_atom line 254
  32. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.plantedDensity_initial_integral line 267
  33. theorem OAI.SKFluctuations.Hierarchy.realGaussianKernel_test_shift line 292
  34. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.planted_test_integrable line 315
  35. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.heat_joint_test_integrable line 322
  36. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.plantedDensity_heat_test line 334
  37. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.plantedDensity_continuation_test_integrable line 357
  38. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.plantedDensity_initial_test line 371
  39. theorem OAI.SKFluctuations.Hierarchy.scalar_restrict_lipschitz line 397
  40. theorem OAI.SKFluctuations.Hierarchy.scalar_clockTest_shiftedMean line 403
  41. theorem OAI.SKFluctuations.Hierarchy.scalar_clockContinuation_shifted line 411
  42. def OAI.SKFluctuations.Hierarchy.HeatJet.plantedIncoming line 418
  43. theorem OAI.SKFluctuations.Hierarchy.HeatJet.plantedIncoming_integrable line 421
  44. theorem OAI.SKFluctuations.Hierarchy.HeatJet.plantedGap_test line 425
  45. def OAI.SKFluctuations.Hierarchy.ScalarPrefixDensity line 462
  46. theorem OAI.SKFluctuations.Hierarchy.scalarPrefixDensity_initial line 469
  47. theorem OAI.SKFluctuations.Hierarchy.scalarPrefixDensity_atom line 492
  48. theorem OAI.SKFluctuations.Hierarchy.scalarPrefixDensity_heat line 530
  49. inductive OAI.SKFluctuations.Hierarchy.ScalarFinitePositivePrefix line 597
  50. theorem OAI.SKFluctuations.Hierarchy.ScalarFinitePositivePrefix.bounds line 604
  51. theorem OAI.SKFluctuations.Hierarchy.ScalarFinitePositivePrefix.density line 612
  52. theorem OAI.SKFluctuations.Hierarchy.ScalarFinitePositivePrefix.density_shape line 640