ShapeMean.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.bounded_product_difference line 12

Source documentation

Product replacement on bounded spin coordinates, with its exact finite sum of coordinate errors.

theorem bounded_product_difference {ι : Type*} (s : Finset ι) (f g : ι → ℝ)
    (hf : ∀ i ∈ s, |f i| ≤ 1) (hg : ∀ i ∈ s, |g i| ≤ 1) :
    |(∏ i ∈ s, f i)-(∏ i ∈ s, g i)| ≤ ∑ i ∈ s, |f i-g i| := by
…

theorem OAI.DilutedSpinGlass.bounded_product_difference_sq line 37

theorem OAI.DilutedSpinGlass.FiniteLaw.product_mean_shift_sq line 53

Source documentation

The one-vertex delay inequality decor:one-vertex-shift. The left side compares independent child continuations with one shared extra transition.

theorem product_mean_shift_sq (P : FiniteLaw Ω) {ι : Type*} [Fintype ι]
    (f : ι → Ω → ℝ) (hf : ∀ i x, |f i x| ≤ 1) :
    ((∏ i, P.expect (f i))-P.expect (fun x => ∏ i, f i x))^2 ≤
      (Fintype.card ι : ℝ)*∑ i, P.covariance (f i) (f i) := by
…

Mentions: OAI.DilutedSpinGlass.FiniteLaw

def OAI.DilutedSpinGlass.PrescribedTree.leafProduct line 75
Source documentation
Every descendant leaf receives the same one-site terminal observable, with its own sampled path.
```
noncomputable def leafProduct : {n : ℕ} → (S : PrescribedTree n) →
    (FinitePath Ω n → ℝ) → Sample Ω S → ℝ
  | 0, .leaf, f, _ => f ()
  | _+1, .node _ C, f, z => ∏ i, leafProduct (C i) (fun y => f ((z i).1,y)) (z i).2

omit [Fintype Ω] in
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample
theorem OAI.DilutedSpinGlass.PrescribedTree.leafProduct_eq_prod line 81

def OAI.DilutedSpinGlass.PrescribedTree.treeMean line 95

Source documentation

Recursive conditional mean of a descendant spin product.

noncomputable def treeMean : {n : ℕ} → (S : PrescribedTree n) → KernelTower Ω n →
    (FinitePath Ω n → ℝ) → ℝ
  | 0, .leaf, _, f => f ()
  | _+1, .node _ C, T, f => ∏ i, T.1.expect (fun a => treeMean (C i) (T.2 a) (fun y => f (a,y)))

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

theorem OAI.DilutedSpinGlass.PrescribedTree.treeMean_eq_expect line 100
theorem OAI.DilutedSpinGlass.PrescribedTree.leafProduct_bound line 123
theorem OAI.DilutedSpinGlass.PrescribedTree.treeMean_bound line 129
def OAI.DilutedSpinGlass.PrescribedTree.unary line 136
Source documentation
One literal unary stretch; it samples one transition from the original kernel tower rather than introducing independent or replacement disorder.
```
def unary {n : ℕ} (S : PrescribedTree n) : PrescribedTree (n+1) := .node 1 (fun _ => S)
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree
theorem OAI.DilutedSpinGlass.PrescribedTree.treeMean_unary line 138
theorem OAI.DilutedSpinGlass.PrescribedTree.treeMean_one_vertex_shift line 152
Source documentation
Literal delay of a branching vertex. Every child loses one initial unary transition; that transition is instead shared by all the children. Both terms are expectations of the actual prescribed-tree products under the same tower.
```
theorem treeMean_one_vertex_shift {n : ℕ} (k : ℕ+) (C : Fin k → PrescribedTree n)
    (T : KernelTower Ω (n+2)) (f : FinitePath Ω (n+2) → ℝ)
    (hf : ∀ x, |f x| ≤ 1) :
    (treeMean (.node k (fun i => unary (C i))) T f-
      treeMean (unary (.node k C)) T f)^2 ≤
      (k : ℝ)*∑ i, T.1.covariance
        (fun a => treeMean (unary (C i)) (T.2 a) (fun y => f (a,y)))
        (fun a => treeMean (unary (C i)) (T.2 a) (fun y => f (a,y))) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.treeMean, OAI.DilutedSpinGlass.PrescribedTree.unary
theorem OAI.DilutedSpinGlass.PrescribedTree.treeMean_node_difference_sq line 179
Source documentation
Propagation to an ancestral branching vertex consists only of conditional expectation and bounded products. This squared contraction estimate is uniform in the transition probabilities and the number of sites.
```
theorem treeMean_node_difference_sq {n : ℕ} (k : ℕ+)
    (C D : Fin k → PrescribedTree n) (T : KernelTower Ω (n+1))
    (f : FinitePath Ω (n+1) → ℝ) (hf : ∀ x, |f x| ≤ 1) :
    (treeMean (.node k C) T f-treeMean (.node k D) T f)^2 ≤
      (k : ℝ)*∑ i, T.1.expect (fun a =>
        (treeMean (C i) (T.2 a) (fun y => f (a,y))-
          treeMean (D i) (T.2 a) (fun y => f (a,y)))^2) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.treeMean