PoissonVariance.lean`

46 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.physical_marked_palm line 17

Source documentation

Palm identity for the actual finite selected-type marked reservoir statistic. No permutation or add-one property of the score is assumed. The base tower and base weight are unchanged on the right: all the other types remain present.

theorem physical_marked_palm {L : ℕ} (S : PrescribedTree L) (a : S.Leaf)
    (r : ℝ≥0) (P : FiniteLaw I) (T : KernelTower Ω L) (Q : Fin L → FiniteLaw A)
    (m : Fin L → ℝ) (base : FinitePath Ω L → ℝ)
    (factor numerator : I → FinitePath Ω L → FinitePath A L → ℝ)
    (f : (S.Leaf → FinitePath Ω L) → ℝ) {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) :
    (∫ n : ℕ, (FiniteLaw.pi (fun _ : Fin n => P)).expect (fun roots =>
      ∑ q, markedTreeScore S a T Q m base roots factor numerator f q) ∂poissonMeasure r) =
    (r : ℝ) * ∫ n : ℕ, P.expect (fun i =>
      (FiniteLaw.pi (fun _ : Fin n => P)).expect (fun roots =>
        markedTreeScore S a T Q m base (Fin.cons i roots) factor numerator f 0))
…

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

def OAI.DilutedSpinGlass.markPrior line 42

Source documentation

An independent mark prior with no physical state.

noncomputable def markPrior : (L : ℕ) → (Fin L → FiniteLaw A) → KernelTower A L
  | 0, _ => ()
  | L+1, Q => (Q 0, fun _ => markPrior L (fun j => Q j.succ))

/-- Move the distinguished Poisson-rooted mark out of the old mark row. -/

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

def OAI.DilutedSpinGlass.splitRow line 47
Source documentation
Move the distinguished Poisson-rooted mark out of the old mark row.
```
def splitRow (k : ℕ) : (Ω × (Fin (k+1) → A)) ≃ ((Ω × (Fin k → A)) × A) where
…
```
theorem OAI.DilutedSpinGlass.markedTower_split line 55
Source documentation
Counts n+1 in the Palm model have exactly the original n-mark law times one unused independent prior process. No term is removed from the base law.
```
theorem markedTower_split (k L : ℕ) (T : KernelTower Ω L) (Q : Fin L → FiniteLaw A) :
    KernelTower.transport (splitRow k) L (markedTower (k+1) L T Q) =
      KernelTower.prod L (markedTower k L T Q) (markPrior L Q) := by
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.KernelTower.transport, OAI.DilutedSpinGlass.splitRow, OAI.DilutedSpinGlass.markedTower, OAI.DilutedSpinGlass.KernelTower.prod, OAI.DilutedSpinGlass.markPrior
theorem OAI.DilutedSpinGlass.physicalPath_split line 73
theorem OAI.DilutedSpinGlass.markPath_split_succ line 84
theorem OAI.DilutedSpinGlass.markPath_split_zero line 96

def OAI.DilutedSpinGlass.insertedMarkedLog line 109

Source documentation

Logarithmic weight after one truly independent added factor on the base which still contains all original selected-type terms.

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

Mentions: OAI.DilutedSpinGlass.FinitePath

theorem OAI.DilutedSpinGlass.insertedMarkedLog_split line 117

def OAI.DilutedSpinGlass.markedRoot line 132

Source documentation

The actual quenched root free energy of the marked model.

noncomputable def markedRoot (T : KernelTower Ω L) (Q : Fin L → FiniteLaw A)
    (m : Fin L → ℝ) (base : FinitePath Ω L → ℝ) (roots : Fin k → I)
    (factor : I → FinitePath Ω L → FinitePath A L → ℝ) : ℝ :=
…

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

theorem OAI.DilutedSpinGlass.markedRoot_cons_bound line 139

Source documentation

Add/delete a marked Poisson point using a common product prior; the old mark row is not reweighted before the comparison.

theorem markedRoot_cons_bound (T : KernelTower Ω L) (Q : Fin L → FiniteLaw A)
    (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
    (base : FinitePath Ω L → ℝ) (roots : Fin k → I) (i : I)
    (factor : I → FinitePath Ω L → FinitePath A L → ℝ) {C : ℝ}
    (hfactor : ∀ x y, |Real.log (factor i x y)| ≤ C) :
    |markedRoot T Q m base (Fin.cons i roots) factor -
      markedRoot T Q m base roots factor| ≤ C := by
…

Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.markedRoot

theorem OAI.DilutedSpinGlass.markedRoot_base_stability line 161

Source documentation

Replacing a physical root block acts only on the base log weight.

theorem markedRoot_base_stability (T : KernelTower Ω L) (Q : Fin L → FiniteLaw A)
    (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
    (base base' : FinitePath Ω L → ℝ) (roots : Fin k → I)
    (factor : I → FinitePath Ω L → FinitePath A L → ℝ) {C : ℝ}
    (hb : ∀ x, |base x - base' x| ≤ C) :
    |markedRoot T Q m base roots factor - markedRoot T Q m base' roots factor| ≤ C := by
…

Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.markedRoot

theorem OAI.DilutedSpinGlass.markedRoot_update_bound line 172

Source documentation

One changed type/site label changes exactly one bounded log factor.

theorem markedRoot_update_bound (T : KernelTower Ω L) (Q : Fin L → FiniteLaw A)
    (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
    (base : FinitePath Ω L → ℝ) (roots : Fin k → I) (q : Fin k) (i : I)
    (factor : I → FinitePath Ω L → FinitePath A L → ℝ) {C : ℝ}
    (hf : ∀ x y, |Real.log (factor i x y) - Real.log (factor (roots q) x y)| ≤ C) :
    |markedRoot T Q m base (Function.update roots q i) factor -
      markedRoot T Q m base roots factor| ≤ C := by
…

Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.markedRoot

def OAI.DilutedSpinGlass.rootArray line 204
Source documentation
The recursive independent-root product and the finite indexed root array are the same labeled data. No exchangeability is needed here.
```
def rootArray {I : Type*} : (n : ℕ) → RootPath I n → Fin n → I
  | 0, _ => Fin.elim0
  | n+1, x => Fin.cons x.1 (rootArray n x.2)
```
Mentions: OAI.DilutedSpinGlass.RootPath
theorem OAI.DilutedSpinGlass.rootArray_replace line 208
instance OAI.DilutedSpinGlass.rootPathCountable line 225
instance OAI.DilutedSpinGlass.rootPathSingleton line 231

theorem OAI.DilutedSpinGlass.markedRoot_count_bound line 241

Source documentation

A linear bound in the actual random point count, from the prior coupling.

theorem markedRoot_count_bound (T : KernelTower Ω L) (Q : Fin L → FiniteLaw A)
    (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
    (base : FinitePath Ω L → ℝ)
    (factor : I → FinitePath Ω L → FinitePath A L → ℝ) {C : ℝ}
    (hf : ∀ i x y, |Real.log (factor i x y)| ≤ C) (n : ℕ) (x : RootPath I n) :
    |markedRoot T Q m base (rootArray n x) factor| ≤
      |markedRoot T Q m base (fun j : Fin 0 => j.elim0) factor| + (n : ℝ)*C := by
…

Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.markedRoot, OAI.DilutedSpinGlass.rootArray

theorem OAI.DilutedSpinGlass.markedRoot_poisson_variance line 266

Source documentation

Literal random-count marked-root concentration. The auxiliary rows change with the count, and their comparison is justified by markedRoot_cons_bound, not by an assumed concentration of an already averaged auxiliary score.

theorem markedRoot_poisson_variance [MeasurableSpace I] [Countable I]
    [MeasurableSingletonClass I] (μ : Measure I) [IsProbabilityMeasure μ] (r : ℝ≥0)
    (T : KernelTower Ω L) (Q : Fin L → FiniteLaw A)
    (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
    (base : FinitePath Ω L → ℝ)
    (factor : I → FinitePath Ω L → FinitePath A L → ℝ) {C : ℝ}
    (hC : 0 ≤ C) (hf : ∀ i x y, |Real.log (factor i x y)| ≤ C) :
    let F := fun n (x : RootPath I n) => markedRoot T Q m base (rootArray n x) factor
…

theorem OAI.DilutedSpinGlass.FiniteLaw.measurable_expect line 305
theorem OAI.DilutedSpinGlass.FiniteLaw.measurable_logMean line 310
theorem OAI.DilutedSpinGlass.KernelTower.measurable_backwardLog line 320
theorem OAI.DilutedSpinGlass.measurable_rootArray line 334
Source documentation
Coordinate evaluation is measurable for the genuine independent root product, including arbitrary (not necessarily discrete) interaction marks.
```
theorem measurable_rootArray {I : Type*} [MeasurableSpace I] (n : ℕ) (j : Fin n) :
    Measurable (fun x : RootPath I n => rootArray n x j) := by
…
```
Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.rootArray
theorem OAI.DilutedSpinGlass.measurable_markedRoot line 345

theorem OAI.DilutedSpinGlass.markedRoot_poisson_variance_measurable line 360

Source documentation

Physical-root concentration for general measurable interaction labels. In particular no finite-support or countability condition is imposed on the bounded physical disorder by this application of the random-count bound.

theorem markedRoot_poisson_variance_measurable
    (μ : Measure I) [IsProbabilityMeasure μ] (r : ℝ≥0)
    (T : KernelTower Ω L) (Q : Fin L → FiniteLaw A)
    (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
    (base : FinitePath Ω L → ℝ)
    (factor : I → FinitePath Ω L → FinitePath A L → ℝ)
    (hfmeas : ∀ x y, Measurable (fun i => factor i x y)) {C : ℝ}
    (hC : 0 ≤ C) (hf : ∀ i x y, |Real.log (factor i x y)| ≤ C) :
    let F := fun n (x : RootPath I n) => markedRoot T Q m base (rootArray n x) factor
…

def OAI.DilutedSpinGlass.poissonRootAverage line 400
Source documentation
Root averaging followed by the genuine Poisson count average.
```
noncomputable def poissonRootAverage (r : ℝ≥0)
    (F : (n : ℕ) → RootPath Ω n → ℝ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.RootPath
theorem OAI.DilutedSpinGlass.measurable_poissonRootAverage line 406
Source documentation
A parameter in a Poisson root average stays measurable, despite the count-dependent dimension of the actual root state.
```
theorem measurable_poissonRootAverage (r : ℝ≥0)
    {F : X → (n : ℕ) → RootPath Ω n → ℝ}
    (hF : ∀ n, Measurable (fun z : X × RootPath Ω n => F z.1 n z.2)) :
    Measurable (fun x => poissonRootAverage μ r (F x)) := by
…
```
Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.poissonRootAverage

theorem OAI.DilutedSpinGlass.poisson_root_second_moment line 420

Source documentation

The actual random-count squared displacement around any center. Both conditional root fluctuations and random-count fluctuations are retained.

theorem poisson_root_second_moment (r : ℝ≥0)
    {F : (n : ℕ) → RootPath Ω n → ℝ} {B : ℕ → ℝ} {C D : ℝ}
    (hF : ∀ n, Measurable (F n)) (hB : ∀ n x, |F n x| ≤ B n)
    (hD : 0 ≤ D)
    (hrep : ∀ n (i : Fin n) x y, |F n x-F n (replaceRoot n x i y)| ≤ C)
    (hadd : ∀ n x y, |F (n+1) (x,y)-F n y| ≤ D) (c : ℝ) :
    (∫ n : ℕ, ∫ x, (F n x-c)^2 ∂rootLaw n (fun _ => μ) ∂poissonMeasure r) ≤
      (C^2/2+D^2)*(r : ℝ) + (poissonRootAverage μ r F-c)^2 := by
…

Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.replaceRoot, OAI.DilutedSpinGlass.rootLaw, OAI.DilutedSpinGlass.poissonRootAverage

theorem OAI.DilutedSpinGlass.independent_block_poisson_variance line 454

Source documentation

Full physical-root variance, with an extra independent root block. It is not conditioned on the Poisson count or on the other root disorder.

theorem independent_block_poisson_variance (r : ℝ≥0) (ν : Measure X)
    [IsProbabilityMeasure ν] {F : X → (n : ℕ) → RootPath Ω n → ℝ}
    {B : ℕ → ℝ} {C D : ℝ}
    (hF : ∀ x n, Measurable (F x n)) (hB : ∀ x n y, |F x n y| ≤ B n)
    (hD : 0 ≤ D)
    (hrep : ∀ x n (i : Fin n) y z, |F x n y-F x n (replaceRoot n y i z)| ≤ C)
    (hadd : ∀ x n y z, |F x (n+1) (y,z)-F x n z| ≤ D)
    (hmean : MemLp (fun x => poissonRootAverage μ r (F x)) 2 ν) :
    (∫ x, ∫ n : ℕ, ∫ y, (F x n y-(∫ z, poissonRootAverage μ r (F z) ∂ν))^2
      ∂rootLaw n (fun _ => μ) ∂poissonMeasure r ∂ν) ≤
      (C^2/2+D^2)*(r : ℝ) + variance (fun x => poissonRootAverage μ r (F x)) ν := by
…

Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.replaceRoot, OAI.DilutedSpinGlass.poissonRootAverage, OAI.DilutedSpinGlass.rootLaw

theorem OAI.DilutedSpinGlass.poissonRootAverage_bound line 480
Source documentation
A linear root bound is sufficient for all count averages in the physical model; no bounded support for the Poisson count is introduced.
```
theorem poissonRootAverage_bound (r : ℝ≥0)
    {F : (n : ℕ) → RootPath Ω n → ℝ} {A D : ℝ}
    (hB : ∀ n x, |F n x| ≤ A+D*n) :
    |poissonRootAverage μ r F| ≤ A+D*(r : ℝ) := by
…
```
Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.poissonRootAverage

theorem OAI.DilutedSpinGlass.poissonRootAverage_stability line 496

Source documentation

Uniform stability passes through the entire marked-Poisson root law.

theorem poissonRootAverage_stability (r : ℝ≥0)
    {F G : (n : ℕ) → RootPath Ω n → ℝ} {A B D : ℝ}
    (hF : ∀ n, Measurable (F n)) (hG : ∀ n, Measurable (G n))
    (hBF : ∀ n x, |F n x| ≤ A+B*n) (hBG : ∀ n x, |G n x| ≤ A+B*n)
    (hdiff : ∀ n x, |F n x-G n x| ≤ D) :
    |poissonRootAverage μ r F-poissonRootAverage μ r G| ≤ D := by
…

Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.poissonRootAverage

theorem OAI.DilutedSpinGlass.markedRoot_uniform_bound line 526

Source documentation

A bound for the root log partition uniform also in the physical base.

theorem markedRoot_uniform_bound (T : KernelTower Ω L) (Q : Fin L → FiniteLaw A)
    (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
    (base : FinitePath Ω L → ℝ) (factor : I → FinitePath Ω L → FinitePath A L → ℝ)
    {B C : ℝ} (hb : ∀ y, |base y| ≤ B)
    (hf : ∀ i x y, |Real.log (factor i x y)| ≤ C) (n : ℕ) (x : RootPath I n) :
    |markedRoot T Q m base (rootArray n x) factor| ≤ B+C*n := by
…

theorem OAI.DilutedSpinGlass.measurable_markedRoot_base line 549

Source documentation

Joint measurability in physical fields and in the actual independent Poisson labels; no discrete-law assumption occurs.

theorem measurable_markedRoot_base (T : KernelTower Ω L) (Q : Fin L → FiniteLaw A)
    (m : Fin L → ℝ) (base : X → FinitePath Ω L → ℝ)
    (hb : ∀ y, Measurable (fun x => base x y))
    (factor : I → FinitePath Ω L → FinitePath A L → ℝ)
    (hf : ∀ x y, Measurable (fun i => factor i x y)) (n : ℕ) :
    Measurable (fun z : X × RootPath I n => markedRoot T Q m (base z.1) (rootArray n z.2) factor) := by
…

theorem OAI.DilutedSpinGlass.markedRoot_full_variance line 564

Source documentation

Unconditional root concentration for the actual marked model with an independent block of physical fields. The old and fresh mark priors change with the Poisson count and are not averaged before the log partition.

theorem markedRoot_full_variance
    (μ : Measure I) [IsProbabilityMeasure μ] (ν : Fin M → Measure X)
    [∀ i, IsProbabilityMeasure (ν i)] (r : ℝ≥0)
    (T : KernelTower Ω L) (Q : Fin L → FiniteLaw A)
    (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
    (base : RootPath X M → FinitePath Ω L → ℝ)
    (hbmeas : ∀ y, Measurable (fun x => base x y))
    (factor : I → FinitePath Ω L → FinitePath A L → ℝ)
    (hfmeas : ∀ x y, Measurable (fun i => factor i x y))
    {B C : ℝ} (hC : 0 ≤ C) (hb : ∀ x y, |base x y| ≤ B)
    (hf : ∀ i x y, |Real.log (factor i x y)| ≤ C)
    (E : Fin M → ℝ)
…

Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.FinitePath

def OAI.DilutedSpinGlass.FiniteLaw.point line 627
theorem OAI.DilutedSpinGlass.FiniteLaw.expect_point line 633
theorem OAI.DilutedSpinGlass.FiniteLaw.logMean_point line 637
def OAI.DilutedSpinGlass.FiniteLaw.uniform line 641
theorem OAI.DilutedSpinGlass.FiniteLaw.logMean_uniform line 646
def OAI.DilutedSpinGlass.KernelTower.terminalTower line 661
Source documentation
Auxiliary levels contain no physical spin randomness. The last level is exactly the Gibbs sum under its uniform spin prior.
```
noncomputable def terminalTower (a : Ω) (P : FiniteLaw Ω) : (r : ℕ) → KernelTower Ω (r+1)
  | 0 => (P, fun _ => ())
  | r+1 => (FiniteLaw.point a, fun _ => terminalTower a P r)
```
Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw.point
def OAI.DilutedSpinGlass.KernelTower.terminalState line 665
theorem OAI.DilutedSpinGlass.KernelTower.backwardLog_terminalTower line 669
theorem OAI.DilutedSpinGlass.backwardLog_marked_base line 685
theorem OAI.DilutedSpinGlass.markedRoot_distance_base line 709
theorem OAI.DilutedSpinGlass.backwardLog_physical line 730

theorem OAI.DilutedSpinGlass.markedRoot_physical_distance line 743

Source documentation

Perturbing the actual finite Ising system changes its hierarchical root logarithm by the sum of the bounded perturbation log-factors.

theorem markedRoot_physical_distance {p N k n : ℕ} {A I : Type} [Fintype A]
    (theta : Fin k → InteractionSample p) (h : Fin N → ℝ)
    (indices : Fin k → Fin p → Fin N) (r : ℕ)
    (Q : Fin (r+1) → FiniteLaw A) (m : Fin (r+1) → ℝ)
    (hm : ∀ j, 0 < m j) (hend : m (Fin.last r) = 1) (roots : Fin n → I)
    (factor : I → FinitePath (Fin N → Spin) (r+1) → FinitePath A (r+1) → ℝ) {C : ℝ}
    (hf : ∀ i x y, |Real.log (factor i x y)| ≤ C) :
    |markedRoot (KernelTower.terminalTower (fun _ : Fin N => false) FiniteLaw.uniform r)
      Q m (fun y => logWeight theta h indices (KernelTower.terminalState r y)) roots factor
        +N*Real.log 2-logPartition theta h indices| ≤ C*n := by
…

Mentions: OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.markedRoot, OAI.DilutedSpinGlass.KernelTower.terminalTower, OAI.DilutedSpinGlass.FiniteLaw.uniform, OAI.DilutedSpinGlass.logWeight, OAI.DilutedSpinGlass.KernelTower.terminalState, OAI.DilutedSpinGlass.logPartition