OAI/Probability/IsingPerceptron/OrderedQuantile.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Ordered Quantile.

  1. lemma OAI.IsingPerceptron.map_restrict_fst_rectangle line 16
  2. lemma OAI.IsingPerceptron.map_restrict_snd_rectangle line 23
  3. lemma OAI.IsingPerceptron.measure_pair_eq_of_lower_rectangles line 30
  4. lemma OAI.IsingPerceptron.ordered_pair_cdf line 51
  5. lemma OAI.IsingPerceptron.pair_quantile_cdf line 80
  6. theorem OAI.IsingPerceptron.ordered_pair_quantile_law line 97
  7. def OAI.IsingPerceptron.treeTail line 129
  8. lemma OAI.IsingPerceptron.continuous_treeTail line 131
  9. lemma OAI.IsingPerceptron.treeTail_mem line 134
  10. lemma OAI.IsingPerceptron.treeTail_level line 137
  11. lemma OAI.IsingPerceptron.treeTail_overlap line 147
  12. lemma OAI.IsingPerceptron.enrichedArrayLaw_treeTail line 153
  13. def OAI.IsingPerceptron.treeLevels line 178
  14. lemma OAI.IsingPerceptron.isClosed_treeLevels line 180
  15. lemma OAI.IsingPerceptron.treeOverlap_mem_levels line 182
  16. lemma OAI.IsingPerceptron.enrichedArrayLaw_treeLevels line 185
  17. theorem OAI.IsingPerceptron.enrichedArrayLaw_limit_tree line 197
  18. lemma OAI.IsingPerceptron.treeTail_eq_level_indicator line 231
  19. lemma OAI.IsingPerceptron.cdf_of_treeTail line 237
  20. lemma OAI.IsingPerceptron.quantile_treeTail line 253
  21. theorem OAI.IsingPerceptron.ordered_pair_tree_tail_integral line 275
  22. lemma OAI.IsingPerceptron.enrichedMeanPressure_field_cost line 319
  23. def OAI.IsingPerceptron.finiteFieldPath line 346
  24. lemma OAI.IsingPerceptron.finiteFieldPath_last line 349
  25. lemma OAI.IsingPerceptron.finiteFieldPath_nonneg line 352
  26. lemma OAI.IsingPerceptron.monotone_finiteFieldPath line 355
  27. lemma OAI.IsingPerceptron.finiteFieldPath_add line 365
  28. lemma OAI.IsingPerceptron.finiteFieldPath_sub line 373
  29. lemma OAI.IsingPerceptron.enrichedMeanPressure_field_lipschitz line 381
  30. lemma OAI.IsingPerceptron.factorial_successor_term line 429
  31. lemma OAI.IsingPerceptron.summable_count_pow_div_factorial line 436
  32. lemma OAI.IsingPerceptron.summable_linear_pow_div_factorial line 442
  33. lemma OAI.IsingPerceptron.summable_growth_exponentialSeries line 450
  34. lemma OAI.IsingPerceptron.hasDerivAt_exponentialSeries line 459
  35. def OAI.IsingPerceptron.poissonMean line 496
  36. lemma OAI.IsingPerceptron.poissonMean_eq_integral line 499
  37. lemma OAI.IsingPerceptron.hasDerivAt_poissonMean line 506
  38. lemma OAI.IsingPerceptron.poissonMean_derivative_bound line 528
  39. theorem OAI.IsingPerceptron.poisson_count_derivative line 540
  40. abbrev OAI.IsingPerceptron.EnrichedFixedData line 567
  41. def OAI.IsingPerceptron.enrichedFixedLaw line 569
  42. instance OAI.IsingPerceptron.enrichedFixedLaw_probability line 573
  43. def OAI.IsingPerceptron.enrichedCountJoin line 578
  44. lemma OAI.IsingPerceptron.enrichedCountJoin_preserving line 581
  45. lemma OAI.IsingPerceptron.poisson_ae_all line 594
  46. lemma OAI.IsingPerceptron.enrichedFixed_pressure_integrable line 603
  47. lemma OAI.IsingPerceptron.enrichedFixed_exp_ae line 616
  48. lemma OAI.IsingPerceptron.abs_cgf_one_le line 629