OAI/Probability/GaussianPropeller/Scalar.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianPropeller.Scalar.charge line 38
  2. theorem OAI.GaussianPropeller.Scalar.third_radius_gt line 40
  3. theorem OAI.GaussianPropeller.Scalar.small_minimum_interval line 50
  4. theorem OAI.GaussianPropeller.Scalar.minimum_gt line 76
  5. theorem OAI.GaussianPropeller.Scalar.first_constraint_rational line 109
  6. theorem OAI.GaussianPropeller.Scalar.final_contradiction line 119
  7. theorem OAI.GaussianPropeller.Scalar.charge_concave line 135
  8. theorem OAI.GaussianPropeller.Scalar.min_charge_le line 143
  9. def OAI.GaussianPropeller.Scalar.finalBudget line 147
  10. theorem OAI.GaussianPropeller.Scalar.finalBudget_concave line 150
  11. theorem OAI.GaussianPropeller.Scalar.clipped_charge line 170
  12. def OAI.GaussianPropeller.Scalar.smallRoot line 193
  13. def OAI.GaussianPropeller.Scalar.threshold line 197
  14. def OAI.GaussianPropeller.Scalar.clipCoeff line 199
  15. theorem OAI.GaussianPropeller.Scalar.smallRoot_five line 201
  16. theorem OAI.GaussianPropeller.Scalar.smallRoot_six line 213
  17. structure OAI.GaussianPropeller.Scalar.Regime line 225
  18. theorem OAI.GaussianPropeller.Scalar.regime_five line 243
  19. theorem OAI.GaussianPropeller.Scalar.regime_six line 264
  20. structure OAI.GaussianPropeller.Scalar.RadiusData line 285
  21. theorem OAI.GaussianPropeller.Scalar.sum_split line 296
  22. theorem OAI.GaussianPropeller.Scalar.sum_prefix_le line 301
  23. theorem OAI.GaussianPropeller.Scalar.RadiusData.radius_le line 311
  24. theorem OAI.GaussianPropeller.Scalar.RadiusData.minimum_le line 314
  25. theorem OAI.GaussianPropeller.Scalar.RadiusData.prefix_norm line 317
  26. theorem OAI.GaussianPropeller.Scalar.RadiusData.prefix_budget line 321
  27. theorem OAI.GaussianPropeller.Scalar.RadiusData.first_two_cap line 325
  28. theorem OAI.GaussianPropeller.Scalar.RadiusData.third_twice line 332
  29. theorem OAI.GaussianPropeller.Scalar.RadiusData.common_charge line 338
  30. theorem OAI.GaussianPropeller.Scalar.RadiusData.tail_coarse_cap line 372
  31. theorem OAI.GaussianPropeller.Scalar.RadiusData.block_budget line 384
  32. theorem OAI.GaussianPropeller.Scalar.RadiusData.prefix_block_budget line 393
  33. theorem OAI.GaussianPropeller.Scalar.RadiusData.prefix_block_norm line 399
  34. theorem OAI.GaussianPropeller.Scalar.RadiusData.minimum_lower line 405
  35. theorem OAI.GaussianPropeller.Scalar.RadiusData.tail_base_charge line 416
  36. theorem OAI.GaussianPropeller.Scalar.RadiusData.fourth_cap line 424
  37. theorem OAI.GaussianPropeller.Scalar.RadiusData.tail_cap line 470
  38. theorem OAI.GaussianPropeller.Scalar.RadiusData.minimum_charge_bound line 475
  39. theorem OAI.GaussianPropeller.Scalar.RadiusData.minimum_le_root line 493
  40. theorem OAI.GaussianPropeller.Scalar.RadiusData.tail_charge line 511
  41. theorem OAI.GaussianPropeller.Scalar.RadiusData.third_large line 524
  42. theorem OAI.GaussianPropeller.Scalar.RadiusData.incompatible line 591
  43. theorem OAI.GaussianPropeller.Scalar.scalar_incompatibility line 605