ColorSymmetry.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.eventually_positive_insertion line 12

lemma OAI.DilutedSpinGlass.PrescribedTree.iteratedFDeriv_anchorAt line 20

Source documentation

The actual iterated Fréchet derivative is the ordered colored expansion. The reverse only records the outermost-first convention of iteratedFDeriv.

lemma iteratedFDeriv_anchorAt {n : ℕ} (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
    (hm : ∀ j : Fin n, m j.succ ≠ 0) (hroot : m 0 = 0) (hend : m (Fin.last n) = 1)
    {ι : Type} [DecidableEq ι] (k : ℕ)
    (S : PrescribedTree n) (U : Finset ι)
    (paths : ι → Sample Ω S → FinitePath Ω n) (G : Sample Ω S → ℝ)
    {A : FinitePath Ω n → ℝ} (hA : ∀ y, 0 < A y) (ds : Fin k → FinitePath Ω n → ℝ) :
    iteratedFDeriv ℝ k (anchorAt S T m U paths G) A ds =
      coloredAt T m (List.ofFn ds).reverse S U paths G A := by
…

Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.anchorAt, OAI.DilutedSpinGlass.PrescribedTree.coloredAt

lemma OAI.DilutedSpinGlass.PrescribedTree.coloredAt_replicate line 42
lemma OAI.DilutedSpinGlass.PrescribedTree.iteratedFDeriv_anchorAt_diagonal line 53

lemma OAI.DilutedSpinGlass.PrescribedTree.coloredAt_reverse_perm line 65

Source documentation

Hence colored histories are symmetric in the actual mixed directions; this is a theorem about the original finite-kernel function.

lemma coloredAt_reverse_perm {n : ℕ} (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
    (hm : ∀ j : Fin n, m j.succ ≠ 0) (hroot : m 0 = 0) (hend : m (Fin.last n) = 1)
    {ι : Type} [DecidableEq ι] {k : ℕ}
    (S : PrescribedTree n) (U : Finset ι)
    (paths : ι → Sample Ω S → FinitePath Ω n) (G : Sample Ω S → ℝ)
    {A : FinitePath Ω n → ℝ} (hA : ∀ y, 0 < A y)
    (ds : Fin k → FinitePath Ω n → ℝ) (π : Equiv.Perm (Fin k)) :
    coloredAt T m (List.ofFn (ds ∘ π)).reverse S U paths G A =
      coloredAt T m (List.ofFn ds).reverse S U paths G A := by
…