OAI/Probability/SKBarriers/Hierarchy/AverageMeanVariance.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SK.Analytic.fieldIndex_eq_natAdd line 16
  2. def OAI.SK.Analytic.blockInteraction line 22
  3. def OAI.SK.Analytic.blockCoefficients line 26
  4. theorem OAI.SK.Analytic.blockInteraction_field line 29
  5. theorem OAI.SK.Analytic.blockCoefficients_field line 34
  6. def OAI.SK.Analytic.blockExponent line 39
  7. theorem OAI.SK.Analytic.blockExponent_field line 42
  8. theorem OAI.SK.Analytic.blockCoefficients_squares line 48
  9. theorem OAI.SK.Analytic.blockExponent_expansion line 58
  10. def OAI.SK.Analytic.blockFieldEnergy line 73
  11. theorem OAI.SK.Analytic.blockFieldEnergy_exponent line 78
  12. theorem OAI.SK.Analytic.blockFieldEnergy_variance line 89
  13. theorem OAI.SK.Analytic.hierarchyGaussian_probability line 118
  14. theorem OAI.SK.Analytic.hierarchyGaussian_path_marginal line 123
  15. theorem OAI.SK.Analytic.pairCoefficients_squared_sum line 132
  16. def OAI.SK.Analytic.sharedBlockWeights line 144
  17. def OAI.SK.Analytic.sharedFieldEnergy line 147
  18. theorem OAI.SK.Analytic.sharedFieldEnergy_expansion line 150
  19. theorem OAI.SK.Analytic.sharedFieldEnergy_variance line 162
  20. theorem OAI.SK.Analytic.blockFieldEnergy_memLp_two line 178
  21. theorem OAI.SK.Analytic.integral_normalized_sum_identity line 199
  22. theorem OAI.SK.Analytic.blockField_coordinate_mean line 217
  23. theorem OAI.SK.Analytic.sharedFieldEnergy_mean line 255
  24. theorem OAI.SK.Analytic.hierarchyMeanSquare_norm_le_one line 299
  25. theorem OAI.SK.Analytic.hierarchyMeanSquare_joint_integrable line 307
  26. theorem OAI.SK.Analytic.sharedFieldEnergy_meanSquare_test line 325
  27. theorem OAI.SK.Analytic.abs_integral_mul_le_sqrt line 380
  28. theorem OAI.SK.Analytic.abs_integral_mul_le_sqrt_of_bound line 391
  29. theorem OAI.SK.Analytic.centered_bounded_test line 410
  30. theorem OAI.SK.Analytic.sharedFieldEnergy_memLp_two line 438
  31. theorem OAI.SK.Analytic.sharedFieldEnergy_centered_test line 465
  32. theorem OAI.SK.Analytic.integral_sqrt_le_sqrt_integral line 514
  33. theorem OAI.SK.Analytic.normalizedSquare_le_const line 532
  34. theorem OAI.SK.Analytic.normalizedSquare_measurable line 545
  35. theorem OAI.SK.Analytic.normalizedDot_measurable line 550
  36. theorem OAI.SK.Analytic.normalizedSquare_memLp line 556
  37. theorem OAI.SK.Analytic.abs_normalizedDot_le_one line 564
  38. theorem OAI.SK.Analytic.mean_variance_from_test line 570
  39. theorem OAI.SK.Analytic.blockMeanSquare_variance line 641
  40. theorem OAI.SK.Analytic.sum_sqrt_increments_le line 683
  41. theorem OAI.SK.Analytic.blockMeanSquare_average_variance line 704