ParameterRate.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.DilutedSpinGlass.HeterogeneousMarks.rootAlphabet line 18
def OAI.DilutedSpinGlass.HeterogeneousMarks.rootTower line 21
def OAI.DilutedSpinGlass.HeterogeneousMarks.rootVector line 29
def OAI.DilutedSpinGlass.HeterogeneousMarks.rootConditionalEnergy line 33
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_rootConditionalEnergy line 47
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.rootConditionalEnergy_bound line 62
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integrable_rootConditionalEnergy line 68
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integrable_rootTreeMean line 76
lemma OAI.DilutedSpinGlass.tendsto_scoreMargin line 94
lemma OAI.DilutedSpinGlass.eventually_scoreMargin_interval line 99

def OAI.DilutedSpinGlass.PhysicalRoot.normalizedParameterError line 118

Source documentation

The actual globally centered dictionary score error, divided by its type intensity. The dictionary, sites, and mark alphabets are allowed to vary with N.

noncomputable def normalizedParameterError
    (μ : (N : ℕ) → Measure (X N)) (ν : (N : ℕ) → Measure (I N)) (ξ : Measure Y)
    (r : ℕ → ℝ≥0) (V : (N : ℕ) → X N → (Fin N → Spin) → ℝ) (field : Y → ℝ)
    (Q : (N : ℕ) → (i : I N) → Fin (L+1) → FiniteLaw (A N i)) (m : Fin (L+1) → ℝ)
    (key : (N : ℕ) → I N → J) (a b t w : J → ℝ)
    (D E : (N : ℕ) → (i : I N) → FinitePath (Fin N → Spin) (L+1) → FinitePath (A N i) (L+1) → ℝ)
    (j : J) (N : ℕ) (u : J → ℝ) : ℝ :=
…

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

lemma OAI.DilutedSpinGlass.PhysicalRoot.normalizedParameterError_nonneg line 142
theorem OAI.DilutedSpinGlass.PhysicalRoot.normalizedParameterError_tendsto line 148
def OAI.DilutedSpinGlass.HeterogeneousMarks.externalTreeScore line 196
Source documentation
The old reservoir and the new insertion factor are distinct arguments. Keeping old fixed is essential when extracting a single analytic function from the entire countable dictionary of insertion parameter values.
```
noncomputable def externalTreeScore (S : PrescribedTree L) (a : S.Leaf)
    (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i)) (m : Fin L → ℝ)
    (base : FinitePath Ω L → ℝ) (roots : Fin n → I) (i : I)
    (old : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
    (new numerator : FinitePath Ω L → FinitePath (A i) L → ℝ)
    (f : (S.Leaf → FinitePath Ω L) → ℝ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.inserted_eq_external line 213

lemma OAI.DilutedSpinGlass.HeterogeneousMarks.external_eq_anchorInsertion line 223

Source documentation

Exact link to the proved all-order anchor Taylor calculus, for arbitrary old disorder and mark alphabets; the old kernels do not vary with new.

lemma external_eq_anchorInsertion (S : PrescribedTree L) (a : S.Leaf)
    (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i)) (m : Fin (L+1) → ℝ)
    (base : FinitePath Ω L → ℝ) (roots : Fin n → I) (i : I)
    (old : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
    (new numerator : FinitePath Ω L → FinitePath (A i) L → ℝ)
    (f : (S.Leaf → FinitePath Ω L) → ℝ) :
    externalTreeScore S a T Q (fun j => m j.succ) base roots i old new numerator f =
      PrescribedTree.anchorInsertion S
        (KernelTower.prod L (KernelTower.tilt L (tower roots L T Q) (fun j => m j.succ)
          (logWeight base roots old)) (markPrior L (Q i))) m a
        (fun x => f (fun b => physical roots L (KernelTower.pathFst L (S.pathAt b x))) *
          numerator (physical roots L (KernelTower.pathFst L (S.pathAt a x)))
…