OAI/Probability/ParisiFinite/SelectedBlock.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Selected Block.

  1. lemma OAI.SKCavity.selectedBlock_support line 60
  2. lemma OAI.SKCavity.arraySupport_Gram line 70
  3. def OAI.SKCavity.UltrametricArrays line 78
  4. lemma OAI.SKCavity.isClosed_UltrametricArrays line 80
  5. theorem OAI.SKCavity.GG_support_ultrametric line 87
  6. theorem OAI.SKCavity.GG_ultrametric line 111
  7. theorem OAI.SKCavity.exists_generic_ultrametric_limit line 125
  8. lemma OAI.SKCavity.pow_sub_lipschitz_unit line 146
  9. lemma OAI.SKCavity.overlap_last_split line 154
  10. lemma OAI.SKCavity.overlap_restrict_difference line 162
  11. def OAI.SKCavity.mixedCavityCoeff line 177
  12. lemma OAI.SKCavity.mixedCavityCoeff_kernel line 183
  13. lemma OAI.SKCavity.mixedCoeff_kernel_add line 197
  14. lemma OAI.SKCavity.mixedCavity_kernel_error line 205
  15. lemma OAI.SKCavity.mixedCavity_diag line 223
  16. theorem OAI.SKCavity.mixedCavity_pressure_error line 231
  17. def OAI.SKCavity.mixedIncrement line 256
  18. lemma OAI.SKCavity.mixedIncrement_difference line 260
  19. def OAI.SKCavity.independentCoeff line 276
  20. lemma OAI.SKCavity.kernel_independent line 279
  21. lemma OAI.SKCavity.increment_independent line 284
  22. lemma OAI.SKCavity.expected_independent_mono line 290
  23. lemma OAI.SKCavity.expected_independent_error line 299
  24. lemma OAI.SKCavity.average_const line 307
  25. lemma OAI.SKCavity.logPartition_restrictLeft line 310
  26. def OAI.SKCavity.liftOld line 319
  27. lemma OAI.SKCavity.expected_liftOld line 321
  28. lemma OAI.SKCavity.increment_le_four_diagonal line 332
  29. def OAI.SKCavity.siteCoeff line 354
  30. lemma OAI.SKCavity.mixedCavity_split line 358
  31. lemma OAI.SKCavity.mixed_core_correction line 368
  32. lemma OAI.SKCavity.skCoeff_abs line 384
  33. lemma OAI.SKCavity.correction_diagonal_le line 388
  34. lemma OAI.SKCavity.core_pressure_lower line 400
  35. theorem OAI.SKCavity.mixedIncrement_lower line 412
  36. lemma OAI.SKCavity.siteCoeff_abs line 420
  37. lemma OAI.SKCavity.siteCoeff_diag_le line 424
  38. theorem OAI.SKCavity.mixedIncrement_upper line 439
  39. lemma OAI.SKCavity.mixedIncrement_bounded line 453
  40. lemma OAI.SKCavity.continuous_expected_coeff line 470
  41. lemma OAI.SKCavity.continuous_mixedIncrement line 495
  42. lemma OAI.SKCavity.sum_fin_increment line 518
  43. lemma OAI.SKCavity.expected_sk_pressure line 529
  44. theorem OAI.SKCavity.sum_mixedIncrement_window line 538
  45. lemma OAI.SKCavity.sum_mixedIncrement_box line 567
  46. lemma OAI.SKCavity.integrable_box_of_bounded line 592
  47. lemma OAI.SKCavity.integral_box_mixedError_le line 598
  48. lemma OAI.SKCavity.exists_box_index_le_integrable line 621
  49. def OAI.SKCavity.coreFluctuationBound line 650
  50. def OAI.SKCavity.coreError line 653
  51. lemma OAI.SKCavity.coreError_integrable line 656
  52. lemma OAI.SKCavity.coreError_dominates line 661
  53. lemma OAI.SKCavity.coreError_nonneg line 671
  54. lemma OAI.SKCavity.integral_coreError_le line 676
  55. def OAI.SKCavity.cavityWindowBudget line 691
  56. theorem OAI.SKCavity.exists_cavity_GG_choice line 697