OAI/Probability/InvariantIsing/Arrays/PerturbationMeasurability.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Jointly measurable Haar-dependent Gaussian tensor fields.

  1. lemma OAI.InvariantIsing.cylinderField_add line 14
  2. lemma OAI.InvariantIsing.cylinderField_single line 18
  3. lemma OAI.InvariantIsing.cylinderField_finset_sum line 22
  4. lemma OAI.InvariantIsing.cylinderField_featureCoefficients line 29
  5. lemma OAI.InvariantIsing.measurable_jointSpectralMonomialField line 35
  6. theorem OAI.InvariantIsing.measurable_jointSpectralMonomialFields line 49

    Source documentation

    This is the joint field measurability required for conditioning Gaussian integration by parts on the random Haar rotation.

    theorem measurable_jointSpectralMonomialFields {N m : ℕ}
    (I : Fin m → Finset (Fin N)) (d : Fin m → ℕ) (n r : ℕ) :
    Measurable (fun p : (SpecialOrthogonal N × (ℕ → ℝ)) × (Spin N × LabeledLeaf n) =>
      cylinderField (jointSpectralMonomialCoefficients (specialRotation p.1.1) I d n r p.2) p.1.2) := by
…

    Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.jointSpectralMonomialCoefficients, OAI.InvariantIsing.specialRotation

  7. lemma OAI.InvariantIsing.measurable_projectedOverlap line 55
  8. theorem OAI.InvariantIsing.measurable_jointSpectralMonomialCovariance line 62