OAI/InformationTheory/BooleanNoise/Comparison.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LeanBlast.CourtadeKumar.le_add_initial_gap_of_deriv_le_on_above line 25
  2. theorem OAI.LeanBlast.CourtadeKumar.le_of_deriv_le_on_above line 61
  3. theorem OAI.LeanBlast.CourtadeKumar.le_of_deriv_le_on_above_of_tendsto line 70
  4. def OAI.LeanBlast.CourtadeKumar.comparisonKernel line 93
  5. def OAI.LeanBlast.CourtadeKumar.comparisonV line 95
  6. def OAI.LeanBlast.CourtadeKumar.comparisonVTime line 98
  7. theorem OAI.LeanBlast.CourtadeKumar.measurable_comparisonKernel line 100
  8. theorem OAI.LeanBlast.CourtadeKumar.comparisonKernel_nonneg line 104
  9. theorem OAI.LeanBlast.CourtadeKumar.comparisonKernel_one line 107
  10. theorem OAI.LeanBlast.CourtadeKumar.comparisonKernel_le line 110
  11. theorem OAI.LeanBlast.CourtadeKumar.intervalIntegrable_comparisonKernel line 122
  12. theorem OAI.LeanBlast.CourtadeKumar.continuousAt_comparisonKernel line 131
  13. theorem OAI.LeanBlast.CourtadeKumar.comparisonV_nonneg line 137
  14. theorem OAI.LeanBlast.CourtadeKumar.comparisonV_le_endpoint_bound line 144
  15. theorem OAI.LeanBlast.CourtadeKumar.tendsto_comparisonVTime_zero line 161
  16. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_comparisonV line 178
  17. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_comparisonVTime line 194
  18. theorem OAI.LeanBlast.CourtadeKumar.sq_lt_one_of_mem line 209
  19. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_artanh_cubic_gap line 213
  20. theorem OAI.LeanBlast.CourtadeKumar.artanh_cubic_lower line 223
  21. def OAI.LeanBlast.CourtadeKumar.rationalArtanhGap line 240
  22. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_rationalArtanhGap line 242
  23. theorem OAI.LeanBlast.CourtadeKumar.artanh_le_rational line 257
  24. def OAI.LeanBlast.CourtadeKumar.comparisonModelKernel line 309
  25. def OAI.LeanBlast.CourtadeKumar.comparisonPrimitive line 311
  26. theorem OAI.LeanBlast.CourtadeKumar.comparisonModelKernel_le line 313
  27. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_comparisonPrimitive line 325
  28. theorem OAI.LeanBlast.CourtadeKumar.continuousAt_comparisonModelKernel line 337
  29. theorem OAI.LeanBlast.CourtadeKumar.integral_comparisonModelKernel line 342
  30. theorem OAI.LeanBlast.CourtadeKumar.comparisonV_lower line 359
  31. theorem OAI.LeanBlast.CourtadeKumar.one_sub_comparisonV_le line 390
  32. def OAI.LeanBlast.CourtadeKumar.comparisonBias line 404
  33. theorem OAI.LeanBlast.CourtadeKumar.comparisonBias_eq line 406
  34. theorem OAI.LeanBlast.CourtadeKumar.comparisonBias_bounds line 411
  35. def OAI.LeanBlast.CourtadeKumar.comparisonLower line 418
  36. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_entropy_exp_neg line 421
  37. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_comparisonLower line 430
  38. theorem OAI.LeanBlast.CourtadeKumar.comparisonLower_pos line 440
  39. theorem OAI.LeanBlast.CourtadeKumar.tendsto_comparisonLower_zero line 448
  40. theorem OAI.LeanBlast.CourtadeKumar.comparisonLower_subsolution line 460
  41. theorem OAI.LeanBlast.CourtadeKumar.comparison_rhs_antitone line 487
  42. theorem OAI.LeanBlast.CourtadeKumar.comparisonLower_le_of_differential_inequality line 494
  43. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_psi_exp_neg line 511
  44. theorem OAI.LeanBlast.CourtadeKumar.small_information_comparison line 521
  45. theorem OAI.LeanBlast.CourtadeKumar.noiseFlow_comparison_lower_from_dissipation line 542
  46. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_noiseFlow_le_comparison_from_dissipation line 568
  47. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_noiseFlow_le_psi_large_from_dissipation line 594
  48. theorem OAI.LeanBlast.CourtadeKumar.dissipation_nonneg line 624
  49. theorem OAI.LeanBlast.CourtadeKumar.antitone_informationDeficit_noiseFlow line 635
  50. theorem OAI.LeanBlast.CourtadeKumar.exp_neg_log_five line 647
  51. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_noiseFlow_le_psi_from_dissipation line 651
  52. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_noise_le_psi_from_dissipation line 695
  53. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_noise_le_psi_from_sharp_dissipation line 713
  54. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_noise_le_psi_of_increasing line 731