FiniteProjection.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.FiniteLaw.Projects line 15
Source documentation
Equality of the finite pushforward law, expressed without choosing a representation of fibers.
```
def Projects (P : FiniteLaw Ω) (Q : FiniteLaw Λ) (π : Ω → Λ) : Prop :=
…
```
Mentions: OAI.DilutedSpinGlass.FiniteLaw
theorem OAI.DilutedSpinGlass.FiniteLaw.Projects.logMean line 18
theorem OAI.DilutedSpinGlass.FiniteLaw.Projects.bind line 24
lemma OAI.DilutedSpinGlass.FiniteLaw.uniform_expect line 31
theorem OAI.DilutedSpinGlass.FiniteLaw.uniform_spin_projection line 38
Source documentation
Forgetting the added spin sends the uniform (N+1)-spin prior exactly to the uniform N-spin prior, including N=0.
```
theorem uniform_spin_projection (N : ℕ) :
    Projects (uniform : FiniteLaw (Fin (N+1) → Spin))
      (uniform : FiniteLaw (Fin N → Spin)) (fun σ i => σ i.succ) := by
…
```
Mentions: OAI.DilutedSpinGlass.FiniteLaw.Projects, OAI.DilutedSpinGlass.FiniteLaw.uniform, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.Spin
def OAI.DilutedSpinGlass.KernelTower.pathMap line 55
def OAI.DilutedSpinGlass.KernelTower.Projects line 61
Source documentation
A genuine prior-law projection at every vertex, not a conclusion about weighted roots.
```
def Projects (π : Ω → Λ) : (n : ℕ) → KernelTower Ω n → KernelTower Λ n → Prop
  | 0, _, _ => True
  | n+1, T, U => FiniteLaw.Projects T.1 U.1 π ∧ ∀ a, Projects π n (T.2 a) (U.2 (π a))
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw.Projects
theorem OAI.DilutedSpinGlass.KernelTower.backwardLog_of_projects line 65
theorem OAI.DilutedSpinGlass.KernelTower.terminalTower_projects line 81
theorem OAI.DilutedSpinGlass.KernelTower.terminalState_pathMap line 93
lemma OAI.DilutedSpinGlass.FiniteLaw.expect_comm line 109
theorem OAI.DilutedSpinGlass.FiniteLaw.product_contraction line 122
Source documentation
Successive projection of independent child vectors in a spatial contraction. This is the actual product law; no decorrelation is assumed.
```
theorem product_contraction {N k : ℕ} {α : Fin k → Type*} [∀ i, Fintype (α i)]
    (P : (i : Fin k) → FiniteLaw (α i)) (X : (i : Fin k) → α i → Fin N → ℝ)
    (hX : ∀ i x v, |X i x v| ≤ 1) (B : Fin N → ℝ) (hB : ∀ v, |B v| ≤ 1) :
    (pi P).l2 (fun x => dot (fun v => (∏ i, X i (x i) v)-
      ∏ i, (P i).expect (fun y => X i y v)) B) ≤
      ∑ i, Real.sqrt (Real.sqrt ((P i).covarianceEnergy (X i))) := by
…
```
Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FiniteLaw.pi, OAI.DilutedSpinGlass.FiniteLaw.l2, OAI.DilutedSpinGlass.FiniteLaw.dot, OAI.DilutedSpinGlass.FiniteLaw.expect, OAI.DilutedSpinGlass.FiniteLaw.covarianceEnergy