NSpinTensorAncestorInput.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The finite Ising tensor application of the conditional marked-path law.

The conditional marked-path law is the finite two-path specialization of Panchenko--Talagrand, C. R. Acad. Sci. Paris I 345 (2007), 653--656, Section 3, Lemma 3.1, equation (8), p.655, and Corollary 3.2, equation (9), p.656. The mark spaces are complete separable metric spaces with their Borel sigma algebras; ancestor conditional distributions may be arbitrary and the measurable terminal need only satisfy E exp X < infinity. The Gaussian-vector terminal satisfies this exponential integrability hypothesis. The law describes the joint branching and marks, including their conditional ancestor distributions.

Averaging the fixed-root law gives the random-root law. Forest edge i has shared mark exactly when i < commonDepth.

theorem OAI.InvariantIsing.tensorFinitePath_exp_integrable line 34

Source documentation

The published marking theorem's exponential integrability hypothesis holds for the actual finite Ising terminal on a finite Gaussian path.

theorem tensorFinitePath_exp_integrable {N m k : ℕ} (hN : 0 < N)
    (eig : Fin N → ℝ) (U : Rotation N) (c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0)
    (z : SpinTensorIndex I degree → ℝ) :
    Integrable (fun w : Fin n → SpinTensorIndex I degree → ℝ =>
      Real.exp (spinTensorTerminal eig U c I degree amplitude (z + ∑ i, w i)))
      (Measure.pi (fun i : Fin n =>
        (tensorGaussianLaw I degree (v i) : Measure (SpinTensorIndex I degree → ℝ)))) := by
…

Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.spinTensorTerminal, OAI.InvariantIsing.tensorGaussianLaw

lemma OAI.InvariantIsing.tensor_abs_integral_bound line 65

def OAI.InvariantIsing.tensorAncestorPairPathMean line 76

Source documentation

Iterated conditional expectation of two Gaussian increment paths. Before their branching depth the two paths receive the same tilted increment; afterwards their next increments are conditionally independent.

def tensorAncestorPairPathMean {N m k : ℕ}
    (eig : Fin N → ℝ) (U : Rotation N) (c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (b : ℕ → ℝ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0) (d : ℕ) :
    (q : ℕ) → ℕ → (SpinTensorIndex I degree → ℝ) → (SpinTensorIndex I degree → ℝ) →
      ((Fin q → (SpinTensorIndex I degree → ℝ) × (SpinTensorIndex I degree → ℝ)) → ℝ) → ℝ
  | 0, _, _, _, F => F Fin.elim0
  | q + 1, i, z₁, z₂, F =>
      if i < d then
        ∫ a, tensorAncestorPairPathMean eig U c I degree amplitude n b v d q (i + 1)
          (z₁ + a) (z₂ + a) (fun w => F (Fin.cons (a, a) w))
          ∂tensorAncestorMarkKernel eig U c I degree amplitude n b v i z₁
…

Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorAncestorMarkKernel

theorem OAI.InvariantIsing.tensorAncestorPairPathMean_abs_le line 94

def OAI.InvariantIsing.tensorTiltedPairPathMean line 125

Source documentation

The actual tilted two-leaf Gaussian path expectation, with the spin residual integrated in the finite Ising terminal.

def tensorTiltedPairPathMean {N m k : ℕ}
    (eig : Fin N → ℝ) (U : Rotation N) (c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (b : ℕ → ℝ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0)
    (z : SpinTensorIndex I degree → ℝ)
    (Φ : ℕ × (Fin n → (SpinTensorIndex I degree → ℝ) × (SpinTensorIndex I degree → ℝ)) → ℝ) : ℝ :=
…

Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex

def OAI.InvariantIsing.TensorAncestorPairLaw line 143
Source documentation
The exact finite tensor specialization of the published joint marked path law. The unperturbed cascade supplies the shared-prefix depth and the normalized ancestor kernels supply the conditional marks.
```
def TensorAncestorPairLaw {N m k : ℕ}
    (eig : Fin N → ℝ) (U : Rotation N) (c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (b : ℕ → ℝ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0) : Prop :=
…
```
Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex
def OAI.InvariantIsing.PanchenkoTalagrandTensorPairInput line 158
Source documentation
Conditional two-path marking law for finite hierarchical tensor fields.
```
def PanchenkoTalagrandTensorPairInput : Prop :=
…
```

theorem OAI.InvariantIsing.tensorRootedPairPath_identity line 168

Source documentation

The independent root Gaussian is averaged after the fixed-root path identity. Root level zero and forest levels one through n agree with the flat tensor coefficient convention.

theorem tensorRootedPairPath_identity (hpub : PanchenkoTalagrandTensorPairInput)
    {N m k : ℕ} (hN : 0 < N)
    (eig : Fin N → ℝ) (U : Rotation N) (c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (b : ℕ → ℝ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0)
    (hb : CascadeExponents n b)
    (Φ : (SpinTensorIndex I degree → ℝ) ×
      (ℕ × (Fin n → (SpinTensorIndex I degree → ℝ) × (SpinTensorIndex I degree → ℝ))) → ℝ)
    (hΦ : Measurable Φ) (hΦb : ∃ C : ℝ, ∀ p, |Φ p| ≤ C) :
    (∫ z, tensorTiltedPairPathMean eig U c I degree amplitude n b (fun i => v (i + 1)) z
      (fun p => Φ (z, p))
      ∂(tensorGaussianLaw I degree (v 0) : Measure (SpinTensorIndex I degree → ℝ))) =
…

Mentions: OAI.InvariantIsing.PanchenkoTalagrandTensorPairInput, OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorTiltedPairPathMean, OAI.InvariantIsing.tensorGaussianLaw