OAI/Probability/IsingPerceptron/CascadePair.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Cascade Pair.

  1. lemma OAI.IsingPerceptron.prefix_pair_value line 18
  2. lemma OAI.IsingPerceptron.cascade_pair_integral line 28
  3. lemma OAI.IsingPerceptron.integral_depth_telescope line 36
  4. theorem OAI.IsingPerceptron.cascade_pair_law_of_tails line 60
  5. def OAI.IsingPerceptron.uniformCellIndex line 89
  6. def OAI.IsingPerceptron.uniformExponent line 90
  7. lemma OAI.IsingPerceptron.uniformExponent_cascade line 92
  8. lemma OAI.IsingPerceptron.measurable_uniformCellIndex line 105
  9. lemma OAI.IsingPerceptron.uniformCellIndex_le line 109
  10. lemma OAI.IsingPerceptron.uniformCellIndex_tail_iff line 111
  11. lemma OAI.IsingPerceptron.unitUniform_Ici_real line 119
  12. lemma OAI.IsingPerceptron.uniformIndex_tail line 130
  13. lemma OAI.IsingPerceptron.cascade_pair_uniformIndex line 138
  14. lemma OAI.IsingPerceptron.uniformCellIndex_eq_floor line 144
  15. lemma OAI.IsingPerceptron.uniformCell_bounds line 152
  16. lemma OAI.IsingPerceptron.uniformCell_left_tendsto line 162
  17. lemma OAI.IsingPerceptron.uniformCell_right_tendsto line 173
  18. def OAI.IsingPerceptron.uniformCellAverage line 188
  19. lemma OAI.IsingPerceptron.uniformCell_measure line 191
  20. lemma OAI.IsingPerceptron.uniformCell_const line 197
  21. lemma OAI.IsingPerceptron.uniformCell_integrable line 202
  22. lemma OAI.IsingPerceptron.uniformCellAverage_bounds line 208
  23. lemma OAI.IsingPerceptron.uniformCellAverage_mem line 226
  24. lemma OAI.IsingPerceptron.uniformCellAverage_monotone line 231
  25. lemma OAI.IsingPerceptron.uniformCellAverage_tendsto line 242
  26. lemma OAI.IsingPerceptron.monotone_ae_continuous_unit line 249
  27. lemma OAI.IsingPerceptron.uniformCellAverage_ae_tendsto line 254
  28. lemma OAI.IsingPerceptron.finite_from_delta_sum line 270
  29. lemma OAI.IsingPerceptron.uniformCellAverage_antiderivative line 279
  30. lemma OAI.IsingPerceptron.uniformCellAverage_tail_sum line 289
  31. lemma OAI.IsingPerceptron.uniformCellAverage_tail_difference line 305
  32. def OAI.IsingPerceptron.scalarNodeTag line 327
  33. def OAI.IsingPerceptron.scalarGaussianNodes line 330
  34. lemma OAI.IsingPerceptron.scalarNodeTag_injective line 333
  35. lemma OAI.IsingPerceptron.scalarGaussianNodes_law line 337
  36. lemma OAI.IsingPerceptron.scalarGaussianRootForest_law line 342
  37. lemma OAI.IsingPerceptron.cylinderField_scalar_nodes line 355
  38. lemma OAI.IsingPerceptron.noiseLeafTerminal_additive line 368
  39. lemma OAI.IsingPerceptron.noiseLeafTerminal_scalar_nodes line 379
  40. lemma OAI.IsingPerceptron.noise_leaf_log_eq_ratio line 399
  41. theorem OAI.IsingPerceptron.bounded_cascade_leaf_recursion line 426
  42. lemma OAI.IsingPerceptron.cascadeRecursion_gaussian line 446
  43. theorem OAI.IsingPerceptron.bounded_gaussian_cascade_leaf_value line 465
  44. abbrev OAI.IsingPerceptron.PositiveCovariance line 488
  45. def OAI.IsingPerceptron.covarianceGaussian line 490
  46. lemma OAI.IsingPerceptron.continuous_covarianceGaussian line 493
  47. lemma OAI.IsingPerceptron.continuous_gaussianMoment line 515
  48. lemma OAI.IsingPerceptron.cylinderCross_comm line 542
  49. lemma OAI.IsingPerceptron.cylinderCross_fin_covariance line 560
  50. lemma OAI.IsingPerceptron.cylinderCross_matrix_posSemidef line 572
  51. lemma OAI.IsingPerceptron.cylinder_vector_law line 583