OAI/Probability/Subsphere/Mixture/BetaTheory.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

Exact beta/gamma independence and products, needed to identify the scalar coordinate laws in the geometric comparison.

  1. lemma OAI.SubsphereCurrent.Mixture.nested_starProjection line 14
  2. lemma OAI.SubsphereCurrent.Mixture.nested_orthogonal_starProjection line 24
  3. lemma OAI.SubsphereCurrent.Mixture.nested_projection_norm line 30
  4. lemma OAI.SubsphereCurrent.Mixture.nested_orthogonal_projection_norm line 34
  5. lemma OAI.SubsphereCurrent.Mixture.nested_rank line 39
  6. def OAI.SubsphereCurrent.Mixture.restrictIso line 44

    Source documentation

    Restriction of an actual ambient orthogonal map to a stable subspace.

    def restrictIso (N : Submodule ℝ E) (e : E ≃ₗᵢ[ℝ] E)
    (he : N.map e.toLinearMap = N) : N ≃ₗᵢ[ℝ] N :=
…
  7. lemma OAI.SubsphereCurrent.Mixture.restrictIso_coe line 49
  8. lemma OAI.SubsphereCurrent.Mixture.stable_map_eq line 53
  9. lemma OAI.SubsphereCurrent.Mixture.haar_scaled_integral line 73
  10. def OAI.SubsphereCurrent.Mixture.perpCoordinate line 87

    Source documentation

    Squared norm of the distinguished perpendicular component.

    def perpCoordinate (V : Submodule ℝ E) (x : E) : ℝ := ‖Vᗮ.orthogonalProjectionOnto x‖^2
  11. lemma OAI.SubsphereCurrent.Mixture.measurable_perpCoordinate line 89
  12. def OAI.SubsphereCurrent.Mixture.mixtureSampler line 94

    Source documentation

    Common direction kernel for all block-invariant spherical laws.

    def mixtureSampler (V : Submodule ℝ E) (z : ℝ × (V × Vᗮ)) : E :=
…
  13. lemma OAI.SubsphereCurrent.Mixture.measurable_mixtureSampler line 97
  14. def OAI.SubsphereCurrent.Mixture.mixtureLaw line 101
  15. lemma OAI.SubsphereCurrent.Mixture.block_average line 105
  16. lemma OAI.SubsphereCurrent.Mixture.block_average_unit line 133
  17. lemma OAI.SubsphereCurrent.Mixture.blockIso_symm line 165
  18. lemma OAI.SubsphereCurrent.Mixture.perpCoordinate_blockIso line 173
  19. lemma OAI.SubsphereCurrent.Mixture.block_left_mem line 180
  20. lemma OAI.SubsphereCurrent.Mixture.block_left_stable line 189
  21. lemma OAI.SubsphereCurrent.Mixture.block_right_fix_e line 197
  22. lemma OAI.SubsphereCurrent.Mixture.block_right_latitude_mem line 201
  23. lemma OAI.SubsphereCurrent.Mixture.block_right_latitude_stable line 209
  24. lemma OAI.SubsphereCurrent.Mixture.latitude_perp_le line 218
  25. lemma OAI.SubsphereCurrent.Mixture.latitude_e_norm line 224
  26. lemma OAI.SubsphereCurrent.Mixture.latitude_rank line 228
  27. lemma OAI.SubsphereCurrent.Mixture.preserving_map_of_intertwining line 244
  28. def OAI.SubsphereCurrent.Mixture.betaSplit line 264
  29. def OAI.SubsphereCurrent.Mixture.betaJoin line 265
  30. def OAI.SubsphereCurrent.Mixture.betaDomain line 266
  31. def OAI.SubsphereCurrent.Mixture.gammaDomain line 267
  32. def OAI.SubsphereCurrent.Mixture.betaSplitDeriv line 269
  33. lemma OAI.SubsphereCurrent.Mixture.betaSplitDeriv_apply line 273
  34. lemma OAI.SubsphereCurrent.Mixture.betaSplit_hasFDeriv line 276
  35. lemma OAI.SubsphereCurrent.Mixture.betaSplit_det line 287
  36. lemma OAI.SubsphereCurrent.Mixture.betaJoin_split line 298
  37. lemma OAI.SubsphereCurrent.Mixture.betaSplit_join line 305
  38. lemma OAI.SubsphereCurrent.Mixture.betaSplit_image line 310
  39. lemma OAI.SubsphereCurrent.Mixture.betaSplit_inj line 320
  40. lemma OAI.SubsphereCurrent.Mixture.lintegral_betaSplit line 324
  41. lemma OAI.SubsphereCurrent.Mixture.gammaPDF_measurable line 347
  42. lemma OAI.SubsphereCurrent.Mixture.betaPDF_measurable line 349
  43. lemma OAI.SubsphereCurrent.Mixture.gamma_beta_density line 352
  44. lemma OAI.SubsphereCurrent.Mixture.lintegral_gamma_eq line 389
  45. lemma OAI.SubsphereCurrent.Mixture.gammaMeasure_restrict_density line 401
  46. lemma OAI.SubsphereCurrent.Mixture.betaMeasure_restrict_density line 408
  47. lemma OAI.SubsphereCurrent.Mixture.lintegral_gamma_prod line 421
  48. lemma OAI.SubsphereCurrent.Mixture.lintegral_beta_gamma line 433
  49. lemma OAI.SubsphereCurrent.Mixture.betaSplit_preserving line 446

    Source documentation

    The exact beta/gamma change of variables as a positive-measure identity.

    lemma betaSplit_preserving {a b : ℝ} (ha : 0 < a) (hb : 0 < b) :
    MeasurePreserving betaSplit ((betaMeasure a b).prod (gammaMeasure (a+b) 1))
      ((gammaMeasure a 1).prod (gammaMeasure b 1)) := by
…

    Mentions: OAI.SubsphereCurrent.Mixture.betaSplit

  50. lemma OAI.SubsphereCurrent.Mixture.square_image_Ioi line 470
  51. lemma OAI.SubsphereCurrent.Mixture.square_inj_Ioi line 478
  52. lemma OAI.SubsphereCurrent.Mixture.lintegral_square line 484
  53. lemma OAI.SubsphereCurrent.Mixture.gamma_square_density line 499
  54. lemma OAI.SubsphereCurrent.Mixture.gamma_sqrt_lintegral line 525
  55. def OAI.SubsphereCurrent.Mixture.gammaSphere line 557

    Source documentation

    A uniform direction with independent squared radius Γ(dim/2,1).

    def gammaSphere : Measure E :=
…
  56. def OAI.SubsphereCurrent.Mixture.gammaSphereConstant line 562
  57. instance OAI.SubsphereCurrent.Mixture.gammaSphere_probability line 567
  58. lemma OAI.SubsphereCurrent.Mixture.gammaSphere_lintegral line 574
  59. lemma OAI.SubsphereCurrent.Mixture.gammaSphere_density line 603
  60. lemma OAI.SubsphereCurrent.Mixture.gammaSphereConstant_ne_top line 611
  61. lemma OAI.SubsphereCurrent.Mixture.invariant_sphere_unique line 629
  62. lemma OAI.SubsphereCurrent.Mixture.measurable_normalize line 650
  63. lemma OAI.SubsphereCurrent.Mixture.normalize_isometry line 655
  64. lemma OAI.SubsphereCurrent.Mixture.normalized_invariant line 659
  65. lemma OAI.SubsphereCurrent.Mixture.isotropic_density_preserving line 691
  66. lemma OAI.SubsphereCurrent.Mixture.normalized_density_uniform line 707
  67. lemma OAI.SubsphereCurrent.Mixture.orthogonal_norm_add line 732
  68. lemma OAI.SubsphereCurrent.Mixture.orthogonal_exp_mul line 738
  69. def OAI.SubsphereCurrent.Mixture.sumGamma line 745
  70. instance OAI.SubsphereCurrent.Mixture.sumGamma_probability line 749
  71. lemma OAI.SubsphereCurrent.Mixture.sumGamma_density line 755
  72. lemma OAI.SubsphereCurrent.Mixture.sumGamma_direction line 773
  73. lemma OAI.SubsphereCurrent.Mixture.gamma_ae_pos line 786
  74. lemma OAI.SubsphereCurrent.Mixture.beta_ae_mem line 790
  75. lemma OAI.SubsphereCurrent.Mixture.beta_gamma_ae_domain line 794
  76. lemma OAI.SubsphereCurrent.Mixture.gamma_prod_ae_domain line 803
  77. lemma OAI.SubsphereCurrent.Mixture.measurable_betaJoin line 812
  78. lemma OAI.SubsphereCurrent.Mixture.betaJoin_preserving line 814
  79. lemma OAI.SubsphereCurrent.Mixture.gamma_ratio_preserving line 827
  80. lemma OAI.SubsphereCurrent.Mixture.gamma_sum_preserving line 835
  81. lemma OAI.SubsphereCurrent.Mixture.gammaSphere_sqnorm line 855
  82. lemma OAI.SubsphereCurrent.Mixture.normalize_sum_sqproj line 889
  83. lemma OAI.SubsphereCurrent.Mixture.sphere_projection_beta line 898