NSpinTensorFrozenFluctuation.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Transfer the actual three-disorder pressure moments to one frozen Gaussian CGF.

lemma OAI.InvariantIsing.joint_map_eq_of_conditional_map_eq line 15
lemma OAI.InvariantIsing.tensorNamespacedLog_conditional_law line 33
lemma OAI.InvariantIsing.measurable_tensorLeafField_joint line 68
lemma OAI.InvariantIsing.measurable_tensorJointLog line 80
lemma OAI.InvariantIsing.measurable_tensorNamespacedLog line 105
lemma OAI.InvariantIsing.measurable_tensorJointFlatLog line 122
def OAI.InvariantIsing.tensorNamespacedPressure line 141

theorem OAI.InvariantIsing.tensorNamespacedPressure_law line 149

Source documentation

The tensor pressure has the marked-cascade pressure law, including the Haar rotation. This is a law identity, stronger than matching means.

theorem tensorNamespacedPressure_law {N m k : ℕ}
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] (eig c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (b : ℕ → ℝ) (treeDegree : Fin k → ℕ) (h : ℕ → ℝ) (hb : CascadeExponents n b) :
    HasLaw (tensorNamespacedPressure eig c I degree amplitude n treeDegree h)
      ((μ.prod (tensorRootTreeLaw I degree n b
        (fun i => tensorPathProfile I degree n treeDegree h (i + 1))
        (tensorPathProfile I degree n treeDegree h 0))).map
          (tensorDisorderPressure eig c I degree amplitude n))
      ((μ.prod (labeledCascadeLaw n b : Measure (LabeledTree n))).prod gaussianCoordinates) := by
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.tensorNamespacedPressure, OAI.InvariantIsing.tensorRootTreeLaw, OAI.InvariantIsing.tensorPathProfile, OAI.InvariantIsing.tensorDisorderPressure

theorem OAI.InvariantIsing.tensorNamespacedPressure_moments line 181

Source documentation

Transport both the second moment and the exact variance and mean.

theorem tensorNamespacedPressure_moments {N m k : ℕ}
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] (eig c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (b : ℕ → ℝ) (treeDegree : Fin k → ℕ) (h : ℕ → ℝ) (hb : CascadeExponents n b)
    (hF : MemLp (tensorDisorderPressure eig c I degree amplitude n) 2
      (μ.prod (tensorRootTreeLaw I degree n b
        (fun i => tensorPathProfile I degree n treeDegree h (i + 1))
        (tensorPathProfile I degree n treeDegree h 0)))) :
    let Q := (μ.prod (labeledCascadeLaw n b : Measure (LabeledTree n))).prod gaussianCoordinates
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.tensorDisorderPressure, OAI.InvariantIsing.tensorRootTreeLaw, OAI.InvariantIsing.tensorPathProfile

theorem OAI.InvariantIsing.tensorFrozenPressure_moments line 205

Source documentation

Freezing one Gaussian namespace preserves the pressure law at every value of that namespace's amplitude, including zero.

theorem tensorFrozenPressure_moments {N m k : ℕ}
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] (eig c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (b : ℕ → ℝ) (treeDegree : Fin k → ℕ) (h : ℕ → ℝ) (hb : CascadeExponents n b)
    (j : Fin k) (t : ℝ)
    (hF : MemLp (tensorDisorderPressure eig c I degree (Function.update amplitude j t) n) 2
      (μ.prod (tensorRootTreeLaw I degree n b
        (fun i => tensorPathProfile I degree n treeDegree h (i + 1))
        (tensorPathProfile I degree n treeDegree h 0)))) :
    let Q := (tensorFrozenLaw μ n b j).prod gaussianCoordinates
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.tensorDisorderPressure, OAI.InvariantIsing.tensorRootTreeLaw, OAI.InvariantIsing.tensorPathProfile, OAI.InvariantIsing.tensorFrozenLaw

lemma OAI.InvariantIsing.tensorFrozenCGF_eq_scaled_difference line 230

theorem OAI.InvariantIsing.tensorFrozenCGF_mean line 248

Source documentation

The expected frozen CGF is the volume times the difference of the two actual all-disorder pressures.

theorem tensorFrozenCGF_mean {N m k : ℕ} (hN : 0 < N)
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] (eig c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (b : ℕ → ℝ) (treeDegree : Fin k → ℕ) (h : ℕ → ℝ)
    (hh : Monotone h) (h0 : 0 ≤ h 0) (hb : CascadeExponents n b) (j : Fin k) (t : ℝ)
    (hF : ∀ a : ℝ, a = t ∨ a = 0 →
      MemLp (tensorDisorderPressure eig c I degree (Function.update amplitude j a) n) 2
        (μ.prod (tensorRootTreeLaw I degree n b
          (fun i => tensorPathProfile I degree n treeDegree h (i + 1))
          (tensorPathProfile I degree n treeDegree h 0)))) :
    let Q := (tensorFrozenLaw μ n b j).prod gaussianCoordinates
…

theorem OAI.InvariantIsing.tensorFrozenCGF_centered_L1_bound line 274

Source documentation

The actual full-disorder pressure variance controls the centered selected-field CGF. The two pressures may be dependent.

theorem tensorFrozenCGF_centered_L1_bound {N m k : ℕ} (hN : 0 < N)
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] (eig c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (b : ℕ → ℝ) (treeDegree : Fin k → ℕ) (h : ℕ → ℝ)
    (hh : Monotone h) (h0 : 0 ≤ h 0) (hb : CascadeExponents n b) (j : Fin k) (t B : ℝ)
    (hF : ∀ a : ℝ, a = t ∨ a = 0 →
      MemLp (tensorDisorderPressure eig c I degree (Function.update amplitude j a) n) 2
        (μ.prod (tensorRootTreeLaw I degree n b
          (fun i => tensorPathProfile I degree n treeDegree h (i + 1))
          (tensorPathProfile I degree n treeDegree h 0))))
    (hv : ∀ a : ℝ, a = t ∨ a = 0 →
      variance (tensorDisorderPressure eig c I degree (Function.update amplitude j a) n)
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.tensorDisorderPressure, OAI.InvariantIsing.tensorRootTreeLaw, OAI.InvariantIsing.tensorPathProfile