OAI/Probability/InvariantIsing/Fields/PriorTensorPressure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual finite tensor perturbation with a fixed spin/leaf prior. The prior may be a normalized spin constraint; it is independent of the rotation.

  1. def OAI.InvariantIsing.priorTensorLog line 13
  2. lemma OAI.InvariantIsing.measurable_priorTensorLog line 21
  3. lemma OAI.InvariantIsing.priorTensorLog_gaussian_memLp line 46
  4. lemma OAI.InvariantIsing.priorTensorLog_gaussian_variance line 63
  5. theorem OAI.InvariantIsing.priorTensorLog_variance line 84

    Source documentation

    The variance constant is independent of the mass and cardinality of an imposed spin constraint.

    theorem priorTensorLog_variance (hhaar : HaarConcentrationInput)
    (hgauss : GaussianLipschitzVarianceInput) :
    ∃ C : ℝ, 0<C ∧ ∀ N : ℕ, 3≤N →
    ∀ μ : Measure (SpecialOrthogonal N), IsProbabilityMeasure μ → μ.IsMulLeftInvariant →
    ∀ m k n : ℕ, ∀ ν : Measure (Spin N × LabeledLeaf n), IsProbabilityMeasure ν →
    ∀ eig c : Fin N → ℝ, ∀ K : ℝ, 0<K → (∀ i, |eig i|≤K) →
    ∀ I : Fin m → Finset (Fin N), ∀ degree : Fin k → Fin m → ℕ,
    ∀ amplitude : Fin k → ℝ, ∀ site : Fin (n+1) → ℝ≥0,
    ∀ monomial : Fin (n+1) → Fin k → ℝ≥0,
      let F := priorTensorLog ν eig c I degree amplitude
…

    Mentions: OAI.InvariantIsing.HaarConcentrationInput, OAI.InvariantIsing.GaussianLipschitzVarianceInput, OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.priorTensorLog