RegularNodeProducer.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.UniversalDictionary.regular_node_pointwise line 19
Source documentation
On every regular admissible parent assignment there is one literal signed matrix experiment. Its geometry is fixed before the physical size and probe parameters are chosen, and its charging constants are independent of the grid. This is the pointwise producer for the averaged decorrelation induction.
```
theorem regular_node_pointwise (M : Model p) (θB hB : ℝ) (L : ℕ)
    (k : ℕ+) (hk : 2≤(k:ℕ)) (C : Fin k → ReducedTopology)
    {η : ℝ} (hη : 0<η) (hlarge : 1<η*(L+1:ℕ))
    (Q : Option (ReducedTopology.node k hk C).Vertex → Fin (L+1))
    (hQ : regularShapeDomain (.node k hk C) (L+1) η Q) :
    ∃ (S T : PrescribedTree (L+1)) (a : S.Leaf)
      (q : Option (Fin (2*Fintype.card (ReducedTopology.node k hk C).Leaf-2+1)) → T.Leaf)
      (J : ℝ), ∀ (N : ℕ) (u : Spec L × ℕ → ℝ),
    η*physicalScheduledEnergy M θB hB N L u (.node k hk C) Q ≤
      4*((L+1:ℕ):ℝ)⁻¹ +
      2*(|physicalTreeMatrixCovariance (gridExponents L) S a M θB hB N u T q|/|J|) +
      4*nodeChargeConstant k hk C η*Real.sqrt (physicalChildMass M θB hB N L u k hk C true Q) +
…
```
Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.UniversalDictionary.physicalScheduledEnergy, OAI.DilutedSpinGlass.UniversalDictionary.physicalTreeMatrixCovariance, OAI.DilutedSpinGlass.UniversalDictionary.gridExponents, OAI.DilutedSpinGlass.UniversalDictionary.physicalChildMass