OAI/Probability/InvariantIsing/Arrays/PerturbationFeatures.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.spectralSpinFeature line 16
2. lemma OAI.InvariantIsing.spectralSpinFeature_cross line 19
3. abbrev OAI.InvariantIsing.SpectralTensorIndex line 29
4. def OAI.InvariantIsing.spectralMonomialFeature line 32
5. theorem OAI.InvariantIsing.spectralMonomialFeature_cross line 38

   Source documentation

   The Gaussian tensor coefficient covariance is exactly the required monomial in the individual spectral overlaps.

   theorem spectralMonomialFeature_cross {N m : ℕ} (U : Rotation N)
       (I : Fin m → Finset (Fin N)) (d : Fin m → ℕ) (σ τ : Spin N) :
       (∑ v : SpectralTensorIndex I d,
         spectralMonomialFeature U I d σ v * spectralMonomialFeature U I d τ v) =
         ∏ a, projectedOverlap U (I a) σ τ ^ d a := by
   …

   Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.Spin, OAI.InvariantIsing.SpectralTensorIndex, OAI.InvariantIsing.spectralMonomialFeature, OAI.InvariantIsing.projectedOverlap

6. theorem OAI.InvariantIsing.spectralMonomial_posSemidef line 49
7. theorem OAI.InvariantIsing.spectralMonomial_abs_le_one line 61
8. lemma OAI.InvariantIsing.measurable_spectralMonomialFeature line 70
9. lemma OAI.InvariantIsing.abs_prod_sub_prod_le_sum line 80
10. lemma OAI.InvariantIsing.abs_pow_sub_pow_le_degree line 107
11. theorem OAI.InvariantIsing.abs_spectralMonomial_sub_rotation_le line 118

    Source documentation

    The covariance, rather than individual Gaussian coefficients, has a dimension-independent rotation modulus.

    theorem abs_spectralMonomial_sub_rotation_le {N m : ℕ} (hN : 0 < N)
        (U V : SpecialOrthogonal N) (I : Fin m → Finset (Fin N)) (d : Fin m → ℕ)
        (σ τ : Spin N) :
        |(∏ a, projectedOverlap (specialRotation U) (I a) σ τ ^ d a) -
          ∏ a, projectedOverlap (specialRotation V) (I a) σ τ ^ d a| ≤
          2 * (∑ a, (d a : ℝ)) * frobeniusDistance U V := by
    …

    Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.projectedOverlap, OAI.InvariantIsing.specialRotation, OAI.InvariantIsing.frobeniusDistance

12. def OAI.InvariantIsing.spectralMonomialCoefficients line 141
13. theorem OAI.InvariantIsing.spectralMonomialCoefficients_cross line 147
14. theorem OAI.InvariantIsing.spectralMonomialCoefficients_variance_le_one line 158
15. def OAI.InvariantIsing.jointSpectralMonomialCoefficients line 166

    Source documentation

    Independent tensor marks at the cascade levels realize the additional tree-overlap power in the paper's joint perturbation kernels.

    def jointSpectralMonomialCoefficients {N m : ℕ} (U : Rotation N)
        (I : Fin m → Finset (Fin N)) (d : Fin m → ℕ) (n r : ℕ)
        (x : Spin N × IsingPerceptron.LabeledLeaf n) : ℕ →₀ ℝ :=
    …

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.Spin, OAI.IsingPerceptron.LabeledLeaf

16. theorem OAI.InvariantIsing.jointSpectralMonomialCoefficients_cross line 173
17. theorem OAI.InvariantIsing.jointSpectralMonomialCoefficients_variance_le_one line 186