TreeDerivatives.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.PrescribedTree.single_expect line 13
Source documentation
A single uncontracted tree samples exactly a whole conditional path.
```
theorem single_expect (n : ℕ) (T : KernelTower Ω n) (D : FinitePath Ω n → ℝ) :
    (sampleLaw (single n) T).expect (fun x => D (singlePath n x)) =
      (KernelTower.law n T).expect D := by
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.PrescribedTree.single, OAI.DilutedSpinGlass.PrescribedTree.singlePath, OAI.DilutedSpinGlass.KernelTower.law
theorem OAI.DilutedSpinGlass.PrescribedTree.bind_expect_cast line 34
theorem OAI.DilutedSpinGlass.PrescribedTree.extension_sampling line 44
Source documentation
The operational extension identity. New descendants are sampled afresh conditional on their shared prefix; no assumption is made about the old test.
```
theorem extension_sampling {n : ℕ} (S : PrescribedTree n) (T : KernelTower Ω n)
    (v : Internal S) (H : Sample Ω S → ℝ) (D : FinitePath Ω n → ℝ) :
    (sampleLaw (grow S v) T).expect (fun x => H (oldSample S v x) * D (newPath S v x)) =
      (sampleLaw S T).expect (fun x => H x * freshEval S T v D x) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.oldSample, OAI.DilutedSpinGlass.PrescribedTree.newPath, OAI.DilutedSpinGlass.PrescribedTree.freshEval
def OAI.DilutedSpinGlass.PrescribedTree.leafSum line 172
Source documentation
Sum of the terminal marks, retaining multiplicity of equal sampled paths.
```
noncomputable def leafSum : {n : ℕ} → (S : PrescribedTree n) →
    (FinitePath Ω n → ℝ) → Sample Ω S → ℝ
  | 0, .leaf, f, _ => f ()
  | _+1, .node _ C, f, x => ∑ i, leafSum (C i) (fun y => f ((x i).1,y)) (x i).2
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample
theorem OAI.DilutedSpinGlass.PrescribedTree.leafSum_eq_sum line 177
theorem OAI.DilutedSpinGlass.PrescribedTree.leafSum_single line 191
theorem OAI.DilutedSpinGlass.PrescribedTree.leafSum_cast line 200
theorem OAI.DilutedSpinGlass.PrescribedTree.leafSum_grow line 210
Source documentation
Exactly one terminal mark is added by growth, and its ancestry is the new path, not a path chosen by equality of sample values.
```
theorem leafSum_grow {n : ℕ} (S : PrescribedTree n) (v : Internal S)
    (f : FinitePath Ω n → ℝ) (x : Sample Ω (grow S v)) :
    leafSum (grow S v) f x = leafSum S f (oldSample S v x) + f (newPath S v x) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.leafSum, OAI.DilutedSpinGlass.PrescribedTree.oldSample, OAI.DilutedSpinGlass.PrescribedTree.newPath
theorem OAI.DilutedSpinGlass.PrescribedTree.sum_gamma line 270
Source documentation
The exact signed budget for internal extensions with finite exponent indices.
```
theorem sum_gamma {n : ℕ} (S : PrescribedTree n) (m : Fin (n+1) → ℝ) :
    (∑ v : Internal S, gamma S m v) = m 0 - (leaves S : ℝ) * m (Fin.last n) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.leaves
theorem OAI.DilutedSpinGlass.PrescribedTree.gamma_nonpos line 290
theorem OAI.DilutedSpinGlass.PrescribedTree.sum_abs_gamma line 308
Source documentation
Absolute coefficients sum to the number of old leaves.
```
theorem sum_abs_gamma {n : ℕ} (S : PrescribedTree n) (m : Fin (n+1) → ℝ)
    (hm : Monotone m) (hpos : ∀ j, 0 ≤ m j)
    (hroot : m 0 = 0) (hend : m (Fin.last n) = 1) :
    (∑ v : Internal S, |gamma S m v|) = (leaves S : ℝ) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.leaves
def OAI.DilutedSpinGlass.PrescribedTree.trivialSample line 320
theorem OAI.DilutedSpinGlass.PrescribedTree.leafSum_const line 324
theorem OAI.DilutedSpinGlass.PrescribedTree.leaves_grow line 333
def OAI.DilutedSpinGlass.PrescribedTree.fullyProtected line 342
Source documentation
All sampled terminal leaves are canceled, with no diagonal contraction.
```
noncomputable def fullyProtected {n : ℕ} (S : PrescribedTree n)
    (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
    (D : FinitePath Ω n → ℝ) (G : Sample Ω S → ℝ) (t : ℝ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample
theorem OAI.DilutedSpinGlass.PrescribedTree.hasDerivAt_fullyProtected line 351
Source documentation
The operational one-step differential recursion underlying every order of the logarithmic and old-replica series.
```
theorem hasDerivAt_fullyProtected {n : ℕ} (S : PrescribedTree 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)
    (D : FinitePath Ω n → ℝ) (G : Sample Ω S → ℝ) (u : ℝ)
    (hu : ∀ y, 0 < 1+u*D y) :
    HasDerivAt (fullyProtected S T m D G)
      (∑ v : Internal S, gamma S m v *
        fullyProtected (grow S v) T m D (fun x => G (oldSample S v x) * D (newPath S v x)) u) u := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.fullyProtected, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.oldSample, OAI.DilutedSpinGlass.PrescribedTree.newPath
def OAI.DilutedSpinGlass.PrescribedTree.extensionIterate line 414
Source documentation
Sum over all sequential genuine fresh-extension histories, with their signed products. This is not a law chosen to force the expansion.
```
noncomputable def extensionIterate {n : ℕ} (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
    (D : FinitePath Ω n → ℝ) :
    ℕ → (S : PrescribedTree n) → (Sample Ω S → ℝ) → ℝ → ℝ
  | 0, S, G, t => fullyProtected S T m D G t
  | k+1, S, G, t => ∑ v : Internal S, gamma S m v *
      extensionIterate T m D k (grow S v) (fun x => G (oldSample S v x) * D (newPath S v x)) t

/-- All orders, in the actual finite path-dependent kernel system. -/
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.fullyProtected, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.oldSample, OAI.DilutedSpinGlass.PrescribedTree.newPath

theorem OAI.DilutedSpinGlass.PrescribedTree.hasDerivAt_extensionIterate line 422

Source documentation

All orders, in the actual finite path-dependent kernel system.

theorem hasDerivAt_extensionIterate {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)
    (D : FinitePath Ω n → ℝ) (k : ℕ) (S : PrescribedTree n) (G : Sample Ω S → ℝ)
    (u : ℝ) (hu : ∀ y, 0 < 1+u*D y) :
    HasDerivAt (extensionIterate T m D k S G) (extensionIterate T m D (k+1) S G u) u := by
…

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