ProductTowers.lean`

43 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.FiniteLaw.transport line 13
Source documentation
Relabeling outcomes does not change a finite conditional probability law.
```
noncomputable def transport (e : Ω ≃ Λ) (P : FiniteLaw Ω) : FiniteLaw Λ where
…
```
Mentions: OAI.DilutedSpinGlass.FiniteLaw
theorem OAI.DilutedSpinGlass.FiniteLaw.expect_transport line 19
theorem OAI.DilutedSpinGlass.FiniteLaw.expMoment_transport line 25
theorem OAI.DilutedSpinGlass.FiniteLaw.logMean_transport line 30
theorem OAI.DilutedSpinGlass.FiniteLaw.tilted_expect_transport line 35
def OAI.DilutedSpinGlass.KernelTower.pathEquiv line 46
theorem OAI.DilutedSpinGlass.KernelTower.pathEquiv_cons line 51
def OAI.DilutedSpinGlass.KernelTower.transport line 54
theorem OAI.DilutedSpinGlass.KernelTower.backwardLog_transport line 60
Source documentation
Conditional power means commute with literal relabeling of every hidden mark variable. This is needed for the physical Palm exchangeability.
```
theorem backwardLog_transport (e : Ω ≃ Λ) (n : ℕ) (T : KernelTower Ω n)
    (m : Fin n → ℝ) (f : FinitePath Λ n → ℝ) :
    backwardLog n (transport e n T) m f =
      backwardLog n T m (f ∘ pathEquiv e n) := by
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.backwardLog, OAI.DilutedSpinGlass.KernelTower.transport, OAI.DilutedSpinGlass.KernelTower.pathEquiv
theorem OAI.DilutedSpinGlass.KernelTower.tiltedExpect_transport line 80
Source documentation
The tilted expectation of any terminal observable is transported along with the quenched log weight. No symmetry assumptions on the weight are used.
```
theorem tiltedExpect_transport (e : Ω ≃ Λ) (n : ℕ) (T : KernelTower Ω n)
    (m : Fin n → ℝ) (f g : FinitePath Λ n → ℝ) :
    (law n (tilt n (transport e n T) m f)).expect g =
      (law n (tilt n T m (f ∘ pathEquiv e n))).expect (g ∘ pathEquiv e n) := by
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.law, OAI.DilutedSpinGlass.KernelTower.tilt, OAI.DilutedSpinGlass.KernelTower.transport, OAI.DilutedSpinGlass.KernelTower.pathEquiv
theorem OAI.DilutedSpinGlass.FiniteLaw.eq_of_weights line 98
theorem OAI.DilutedSpinGlass.FiniteLaw.tilt_transport line 104
theorem OAI.DilutedSpinGlass.KernelTower.tilt_transport line 118

def OAI.DilutedSpinGlass.PrescribedTree.sampleEquiv line 140

Source documentation

Relabel every sampled vertex without identifying distinct replica paths.

def sampleEquiv (e : Ω ≃ Λ) : {n : ℕ} → (S : PrescribedTree n) → Sample Ω S ≃ Sample Λ S
  | 0, .leaf => Equiv.refl _
  | _+1, .node _ C => Equiv.piCongrRight (fun i => e.prodCongr (sampleEquiv e (C i)))

omit [Fintype Ω] [Fintype Λ] in

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample

theorem OAI.DilutedSpinGlass.PrescribedTree.sampleEquiv_node line 145
theorem OAI.DilutedSpinGlass.PrescribedTree.sampleWeight_transport line 149
theorem OAI.DilutedSpinGlass.PrescribedTree.sampleExpect_transport line 166
theorem OAI.DilutedSpinGlass.PrescribedTree.tiltedSampleExpect_transport line 175
theorem OAI.DilutedSpinGlass.PrescribedTree.pathAt_sampleEquiv line 189
Source documentation
A leaf keeps its label under relabeling, even when two sampled paths agree.
```
theorem pathAt_sampleEquiv (e : Ω ≃ Λ) {n : ℕ} (S : PrescribedTree n)
    (a : Leaf S) (x : Sample Ω S) :
    pathAt S a (sampleEquiv e S x) = KernelTower.pathEquiv e n (pathAt S a x) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.pathAt, OAI.DilutedSpinGlass.PrescribedTree.sampleEquiv, OAI.DilutedSpinGlass.KernelTower.pathEquiv
theorem OAI.DilutedSpinGlass.FiniteLaw.ext line 204
theorem OAI.DilutedSpinGlass.FiniteLaw.logMean_bind_fst line 212
Source documentation
A mark block not present in a log weight integrates out, before or after any one power-mean tilt.
```
theorem logMean_bind_fst (P : FiniteLaw Ω) (Q : FiniteLaw Λ) (m : ℝ) (f : Ω → ℝ) :
    (P.bind (fun _ => Q)).logMean m (fun z => f z.1) = P.logMean m f := by
…
```
Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FiniteLaw.logMean
theorem OAI.DilutedSpinGlass.FiniteLaw.tilt_bind_fst line 216
def OAI.DilutedSpinGlass.KernelTower.prod line 234
Source documentation
Independent auxiliary mark kernels are joined at each depth, not added as separately normalized replicas.
```
noncomputable def prod : (n : ℕ) → KernelTower Ω n → KernelTower Λ n →
    KernelTower (Ω × Λ) n
  | 0, _, _ => ()
  | n+1, T, U => (T.1.bind (fun _ => U.1), fun z => prod n (T.2 z.1) (U.2 z.2))
```
Mentions: OAI.DilutedSpinGlass.KernelTower
def OAI.DilutedSpinGlass.KernelTower.pathFst line 239
def OAI.DilutedSpinGlass.KernelTower.pathSnd line 243
theorem OAI.DilutedSpinGlass.KernelTower.backwardLog_prod_fst line 247
theorem OAI.DilutedSpinGlass.KernelTower.tilt_prod_fst line 265
theorem OAI.DilutedSpinGlass.FiniteLaw.expect_pi_perm line 297
Source documentation
Exchangeability of independent identically distributed root marks.
```
theorem expect_pi_perm {ι : Type*} [Fintype ι] [DecidableEq ι]
    (P : FiniteLaw Ω) (σ : Equiv.Perm ι) (F : (ι → Ω) → ℝ) :
    (pi (fun _ : ι => P)).expect (fun x => F (x ∘ σ)) =
      (pi (fun _ : ι => P)).expect F := by
…
```
Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FiniteLaw.pi, OAI.DilutedSpinGlass.FiniteLaw.expect
theorem OAI.DilutedSpinGlass.FiniteLaw.expect_pi_equivariant line 316
Source documentation
All summands of an equivariant marked score have the same mean. This is proved from iid sampling, rather than being a Palm hypothesis.
```
theorem expect_pi_equivariant {n : ℕ} (P : FiniteLaw Ω)
    (F : (Fin n → Ω) → Fin n → ℝ)
    (hF : ∀ (σ : Equiv.Perm (Fin n)) x i, F (x ∘ σ) i = F x (σ i))
    (i j : Fin n) :
    (pi (fun _ : Fin n => P)).expect (fun x => F x i) =
      (pi (fun _ : Fin n => P)).expect (fun x => F x j) := by
…
```
Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FiniteLaw.pi, OAI.DilutedSpinGlass.FiniteLaw.expect

theorem OAI.DilutedSpinGlass.poisson_marked_add_one line 338

Source documentation

The marked Poisson identity used in pert:palm. Each score component may depend on all other marks; only the actual permutation covariance is needed. The new mark is sampled independently with its original prior.

theorem poisson_marked_add_one (r : ℝ≥0) (P : FiniteLaw Ω)
    (F : (n : ℕ) → (Fin n → Ω) → Fin n → ℝ) {B : ℝ}
    (hB : ∀ n x i, |F n x i| ≤ B)
    (hF : ∀ n (σ : Equiv.Perm (Fin n)) x i, F n (x ∘ σ) i = F n x (σ i)) :
    (∫ n : ℕ, (FiniteLaw.pi (fun _ : Fin n => P)).expect (fun x => ∑ i, F n x i)
      ∂poissonMeasure r) =
    (r : ℝ) * ∫ n : ℕ, P.expect (fun y =>
      (FiniteLaw.pi (fun _ : Fin n => P)).expect (fun x => F (n+1) (Fin.cons y x) 0))
      ∂poissonMeasure r := by
…

Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FiniteLaw.pi

def OAI.DilutedSpinGlass.markPerm line 386
Source documentation
Permute selected-type mark labels without permuting spins or other types.
```
def markPerm {k : ℕ} (σ : Equiv.Perm (Fin k)) : (Fin k → A) ≃ (Fin k → A) where
…
```
def OAI.DilutedSpinGlass.rowPerm line 392

def OAI.DilutedSpinGlass.markedTower line 398

Source documentation

The literal product-prior tower for k independent copies of a mark process. The physical tower includes every other type in the reservoir.

noncomputable def markedTower (k : ℕ) : (L : ℕ) → KernelTower Ω L →
    (Fin L → FiniteLaw A) → KernelTower (Ω × (Fin k → A)) L
  | 0, _, _ => ()
  | L+1, T, Q => (T.1.bind (fun _ => FiniteLaw.pi (fun _ : Fin k => Q 0)),
      fun y => markedTower k L (T.2 y.1) (fun j => Q j.succ))

/-- An actual selected-type replica-row prior is permutation invariant. -/

Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FiniteLaw.pi

theorem OAI.DilutedSpinGlass.markedTower_transport line 405
Source documentation
An actual selected-type replica-row prior is permutation invariant.
```
theorem markedTower_transport {k : ℕ} (σ : Equiv.Perm (Fin k)) (L : ℕ)
    (T : KernelTower Ω L) (Q : Fin L → FiniteLaw A) :
    KernelTower.transport (rowPerm σ) L (markedTower k L T Q) = markedTower k L T Q := by
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.KernelTower.transport, OAI.DilutedSpinGlass.rowPerm, OAI.DilutedSpinGlass.markedTower

def OAI.DilutedSpinGlass.physicalPath line 422

Source documentation

Forget the selected auxiliary mark rows.

def physicalPath (k : ℕ) : (L : ℕ) → FinitePath (Ω × (Fin k → A)) L → FinitePath Ω L
  | 0, _ => ()
  | L+1, y => (y.1.1, physicalPath k L y.2)

/-- Read one complete independent mark process from a latent path. -/

Mentions: OAI.DilutedSpinGlass.FinitePath

def OAI.DilutedSpinGlass.markPath line 427

Source documentation

Read one complete independent mark process from a latent path.

def markPath {k : ℕ} (q : Fin k) : (L : ℕ) →
    FinitePath (Ω × (Fin k → A)) L → FinitePath A L
  | 0, _ => ()
  | L+1, y => (y.1.2 q, markPath q L y.2)

omit [Fintype Ω] [Fintype A] in

Mentions: OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.FinitePath

theorem OAI.DilutedSpinGlass.physicalPath_rowPerm line 433
theorem OAI.DilutedSpinGlass.markPath_rowPerm line 444

def OAI.DilutedSpinGlass.markedLog line 457

Source documentation

All k selected factors at a terminal leaf, tilting the complete base log weight.

noncomputable def markedLog (base : FinitePath Ω L → ℝ) (roots : Fin k → I)
    (factor : I → FinitePath Ω L → FinitePath A L → ℝ)
    (y : FinitePath (Ω × (Fin k → A)) L) : ℝ :=
…

Mentions: OAI.DilutedSpinGlass.FinitePath

theorem OAI.DilutedSpinGlass.markedLog_rowPerm line 463
def OAI.DilutedSpinGlass.markedTreeScore line 477
Source documentation
The actual tree score of a specified selected-type term, with an arbitrary old physical replica test. The terminal numerator includes the spin-or-marker anchor from the manuscript, and the factor is its original denominator.
```
noncomputable def markedTreeScore (S : PrescribedTree L) (a : S.Leaf)
    (T : KernelTower Ω L) (Q : Fin L → FiniteLaw A) (m : Fin L → ℝ)
    (base : FinitePath Ω L → ℝ) (roots : Fin k → I)
    (factor numerator : I → FinitePath Ω L → FinitePath A L → ℝ)
    (f : (S.Leaf → FinitePath Ω L) → ℝ) (q : Fin k) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.q

theorem OAI.DilutedSpinGlass.markedTreeScore_perm line 490

Source documentation

The equivariance required by Poisson Palm is proved for the physical tilting statistic; it is not an added hypothesis on the score.

theorem markedTreeScore_perm (S : PrescribedTree L) (a : S.Leaf)
    (T : KernelTower Ω L) (Q : Fin L → FiniteLaw A) (m : Fin L → ℝ)
    (base : FinitePath Ω L → ℝ) (roots : Fin k → I)
    (factor numerator : I → FinitePath Ω L → FinitePath A L → ℝ)
    (f : (S.Leaf → FinitePath Ω L) → ℝ) (σ : Equiv.Perm (Fin k)) (q : Fin k) :
    markedTreeScore S a T Q m base (roots ∘ σ) factor numerator f q =
      markedTreeScore S a T Q m base roots factor numerator f (σ q) := by
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.markedTreeScore

theorem OAI.DilutedSpinGlass.abs_markedTreeScore_le line 511

Source documentation

The score component remains uniformly bounded in the Poisson count. This is the integrability needed for the literal Palm identity.

theorem abs_markedTreeScore_le (S : PrescribedTree L) (a : S.Leaf)
    (T : KernelTower Ω L) (Q : Fin L → FiniteLaw A) (m : Fin L → ℝ)
    (base : FinitePath Ω L → ℝ) (roots : Fin k → I)
    (factor numerator : I → FinitePath Ω L → FinitePath A L → ℝ)
    (f : (S.Leaf → FinitePath Ω L) → ℝ) (q : Fin k) {B : ℝ}
    (hf : ∀ x, |f x| ≤ B) (hn : ∀ i y z, |numerator i y z| ≤ 1)
    (hA : ∀ i y z, 1/2 ≤ factor i y z) :
    |markedTreeScore S a T Q m base roots factor numerator f q| ≤ 2*B := by
…