OAI/Probability/SKFluctuations/GaussianRootTransversality.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Gaussian Root Transversality.

  1. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.rootIntegral_pos_gaussian line 21
  2. def OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.gaussianWeight line 96
  3. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.gaussianWeight_pos line 99
  4. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.gaussianWeight_deriv line 102
  5. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.gaussianWeight_dominated line 109
  6. theorem OAI.SKFluctuations.Scalar.absBounded_ratio line 143
  7. theorem OAI.SKFluctuations.Scalar.physicalSlopeOfJets_bounded line 154
  8. theorem OAI.SKFluctuations.Scalar.physicalSlopeOfJets_lam_continuous line 187
  9. theorem OAI.SKFluctuations.Scalar.physicalSlopeOfJets_second line 197
  10. theorem OAI.SKFluctuations.Scalar.physicalSlopeOfJets_third line 203
  11. def OAI.SKFluctuations.Hierarchy.scalarClockProfileJet line 219
  12. theorem OAI.SKFluctuations.Hierarchy.ScalarClockPhysicalSlice_profG line 227
  13. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileJet_deriv line 233
  14. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileJet_parity line 240
  15. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileJet_one_zero line 249
  16. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileJet_three_zero line 255
  17. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileJet_curvature_pos line 260
  18. def OAI.SKFluctuations.Hierarchy.scalarClockProfileSlice line 272
  19. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileJet_absBounded line 281
  20. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileSlice_polyBounded line 286
  21. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileSlice_lam_continuous line 296
  22. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileJet_zero_upper line 301
  23. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileSlice_root_pos line 310
  24. theorem OAI.SKFluctuations.Hierarchy.integral_pi_one line 340
  25. theorem OAI.SKFluctuations.Hierarchy.scalar_gaussian_density line 352
  26. theorem OAI.SKFluctuations.Hierarchy.scalar_clockTest_density line 363
  27. theorem OAI.SKFluctuations.Hierarchy.scalar_density_partition_pos line 375
  28. theorem OAI.SKFluctuations.Hierarchy.integral_even_eq_two_Ioi line 386
  29. def OAI.SKFluctuations.Hierarchy.realGaussianKernel line 404
  30. theorem OAI.SKFluctuations.Hierarchy.realGaussianKernel_pos line 407
  31. theorem OAI.SKFluctuations.Hierarchy.realGaussianKernel_bridge line 411
  32. theorem OAI.SKFluctuations.Hierarchy.gaussian_heat_factor line 434
  33. theorem OAI.SKFluctuations.Hierarchy.ResidualJet.exp_heat line 471
  34. structure OAI.SKFluctuations.Hierarchy.GaussianResidual line 481
  35. def OAI.SKFluctuations.Hierarchy.GaussianResidual.density line 488
  36. def OAI.SKFluctuations.Hierarchy.GaussianResidual.potential line 491
  37. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.density_pos line 493
  38. def OAI.SKFluctuations.Hierarchy.GaussianResidual.ofVariance line 496
  39. def OAI.SKFluctuations.Hierarchy.GaussianResidual.heat line 498
  40. def OAI.SKFluctuations.Hierarchy.GaussianResidual.atom line 503
  41. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.density_heat line 509
  42. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.density_atom line 517
  43. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.cone_heat line 526
  44. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.cone_atom line 531
  45. theorem OAI.SKFluctuations.Hierarchy.exponentialIncrement_gaussianReal_zero line 546
  46. theorem OAI.SKFluctuations.Hierarchy.realGaussianKernel_continuous line 550
  47. theorem OAI.SKFluctuations.Hierarchy.realGaussianKernel_integrable_iff line 554
  48. theorem OAI.SKFluctuations.Hierarchy.realGaussianKernel_weighted_integrable line 563
  49. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.density_continuous line 570
  50. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.weighted_integrable line 573
  51. theorem OAI.SKFluctuations.Hierarchy.convolution_product_integrable line 581
  52. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.heat_joint_integrable line 595