OAI/Probability/InvariantIsing/Cavity/CavityFrameMoments.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Uniform even moments for the whole fresh-frame projection vector.

  1. def OAI.InvariantIsing.cavityHaarProjections line 13
  2. lemma OAI.InvariantIsing.continuous_cavityHaarProjections line 17
  3. lemma OAI.InvariantIsing.cavityHaarProjections_norm_bound line 33
  4. lemma OAI.InvariantIsing.integrable_cavityHaarProjections_power line 46
  5. lemma OAI.InvariantIsing.cavity_projection_power_le line 57
  6. theorem OAI.InvariantIsing.cavity_frame_even_moment_bound line 67
  7. theorem OAI.InvariantIsing.cavity_frame_even_moment_bound_of_norm line 101
  8. theorem OAI.InvariantIsing.cavity_frame_mixture_even_moment line 119