PairSquare.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.pairObservableHistory_sum line 15
lemma OAI.DilutedSpinGlass.PrescribedTree.pairObservableHistory_div line 33
theorem OAI.DilutedSpinGlass.PrescribedTree.pair_history_dot line 44
Source documentation
The empirical overlap is the physical iid-uniform site average of the literal one-color histories. No independence from the old test is imposed.
```
theorem pair_history_dot (T : KernelTower Ω (n+1)) (m : Fin (n+2) → ℝ)
    (S : PrescribedTree (n+1)) (a : S.Leaf) (d : ℕ)
    (X : FinitePath Ω (n+1) → Fin N → ℝ) (f : Sample Ω S → ℝ) :
    pairObservableHistory T m S a d (fun x y => FiniteLaw.dot (X x) (X y)) f =
      (∑ i : Fin N, shapeHistory T m
        (fun M : Option (Fin 1) → Option (Fin 1) → ℕ => if M none (some 0) = d then 1 else 0)
        (fun _ x => X x i) S a f)/(N:ℝ) := by
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.pairObservableHistory, OAI.DilutedSpinGlass.FiniteLaw.dot, OAI.DilutedSpinGlass.PrescribedTree.shapeHistory
def OAI.DilutedSpinGlass.PrescribedTree.pairFreshCost line 71
lemma OAI.DilutedSpinGlass.PrescribedTree.pairFreshCost_nonneg line 75

theorem OAI.DilutedSpinGlass.PrescribedTree.pair_square_identity line 85

Source documentation

The exact nonnegative-square identity before root averaging. It follows from actual two-path marginals and complete old-law projectivity.

theorem pair_square_identity (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
    (hend : m (Fin.last n) = 1) (S : PrescribedTree n) (a b : S.Leaf)
    (hab : a ≠ b) (htwo : ∀ c : S.Leaf, c = a ∨ c = b)
    (d : ℕ) (hd : d < n) (hsplit : splitDepth S a b = d)
    (R : FinitePath Ω n → FinitePath Ω n → ℝ) :
    (1/2:ℝ) * ∑ v : S.Internal, pairFreshCost S m a d v *
      ((grow S v).sampleLaw T).expect (fun x =>
        (R (S.pathAt a (oldSample S v x)) (S.pathAt b (oldSample S v x)) -
          R ((grow S v).pathAt (oldLeaf S v a) x) ((grow S v).pathAt (newLeaf S v) x))^2) =
      (m ⟨d+1,by omega⟩-m ⟨d,by omega⟩) *
        (S.sampleLaw T).expect (fun x => R (S.pathAt a x) (S.pathAt b x)^2) +
      pairObservableHistory T m S a d R (fun x => R (S.pathAt a x) (S.pathAt b x)) := by
…

def OAI.DilutedSpinGlass.boundParameter line 177
lemma OAI.DilutedSpinGlass.boundParameter_mem line 179
lemma OAI.DilutedSpinGlass.boundParameter_eq line 183
lemma OAI.DilutedSpinGlass.measurable_boundParameter line 186
theorem OAI.DilutedSpinGlass.HeterogeneousMarks.otherLog_congr line 197
theorem OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedRawScore_congr line 210
theorem OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedError_congr line 220

def OAI.DilutedSpinGlass.HeterogeneousMarks.parameterFactor line 237

Source documentation

The entire dictionary factor family, with its original two coordinates and no truncation in the number of types.

noncomputable def parameterFactor {J : Type} (key : I → J) (a b t : J → ℝ)
    (D E : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
    (u : J → ℝ) (i : I) (x : FinitePath Ω L) (y : FinitePath (A i) L) : ℝ :=
…

Mentions: OAI.DilutedSpinGlass.FinitePath

lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_parameterFactor line 244
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.parameterFactor_refresh line 253