ColorIterate.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.contDiffAt_protectedAt line 12
lemma OAI.DilutedSpinGlass.PrescribedTree.contDiffAt_anchorAt line 28
def OAI.DilutedSpinGlass.PrescribedTree.coloredAt line 50
Source documentation
The literal ordered colored extension calculus. Each color either uses one unused old leaf, which is then removed from the available list, or grows one fresh branch with its original signed gamma coefficient.
```
noncomputable def coloredAt {n : ℕ} (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
    {ι : Type} [DecidableEq ι] : List (FinitePath Ω n → ℝ) →
      (S : PrescribedTree n) → Finset ι → (ι → Sample Ω S → FinitePath Ω n) →
        (Sample Ω S → ℝ) → (FinitePath Ω n → ℝ) → ℝ
  | [], S, U, paths, G, A => anchorAt S T m U paths G A
  | D :: ds, S, U, paths, G, A =>
    (∑ i ∈ U, coloredAt T m ds S (U.erase i) paths (fun x => G x * D (paths i x)) A) +
    ∑ v : Internal S, gamma S m v * coloredAt T m ds (grow S v) U
      (fun i x => paths i (oldSample S v x))
      (fun x => G (oldSample S v x) * D (newPath S v x)) A
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.anchorAt, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.oldSample, OAI.DilutedSpinGlass.PrescribedTree.newPath
lemma OAI.DilutedSpinGlass.PrescribedTree.contDiffAt_coloredAt line 61

lemma OAI.DilutedSpinGlass.PrescribedTree.hasDerivAt_coloredAt line 78

Source documentation

Differentiating a colored history inserts the next color at the end of the ordered history. No symmetrization is imposed as a definition.

lemma hasDerivAt_coloredAt {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 ι] (ds : List (FinitePath Ω n → ℝ))
    (S : PrescribedTree n) (U : Finset ι)
    (paths : ι → Sample Ω S → FinitePath Ω n) (G : Sample Ω S → ℝ)
    {A : ℝ → FinitePath Ω n → ℝ} {D : FinitePath Ω n → ℝ} {u : ℝ}
    (hA : ∀ y, 0 < A u y) (hdA : ∀ y, HasDerivAt (fun t => A t y) (D y) u) :
    HasDerivAt (fun t => coloredAt T m ds S U paths G (A t))
      (coloredAt T m (ds ++ [D]) S U paths G (A u)) u := by
…

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

lemma OAI.DilutedSpinGlass.PrescribedTree.fderiv_coloredAt_apply line 99