ShapeCharging.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.branchingCount_of_matrix line 15
Source documentation
A shape specified by a complete labeled splitting matrix contains each of the target's branching vertices, with its vertex multiplicity intact.
```
lemma branchingCount_of_matrix (T S : PrescribedTree L) (q : C → T.Leaf)
    (hq : Function.Surjective q) (pos : C → S.Leaf)
    (h : ∀ a b, splitDepth S (pos a) (pos b) = splitDepth T (q a) (q b))
    (P : ℕ → Prop) : branchingCount T P ≤ branchingCount S P := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.branchingCount

theorem OAI.DilutedSpinGlass.PrescribedTree.prescribed_history_charging_bound line 30

Source documentation

Absolute projection-error cost for the ACTUAL exact-matrix history. This is the charging step in the shifted-two-copy argument: take Q to be shifted depths, so the old tree has no branching in Q. The exponent counts vertices, not distinct depths, hence aligned copies are charged separately.

theorem prescribed_history_charging_bound (hL : 0 < L) (Q : Finset ℕ)
    (T S : PrescribedTree L) (q : C → T.Leaf) (hq : Function.Surjective q)
    (hS : branchingCount S (· ∈ Q) = 0)
    (W : (R : PrescribedTree L) → (C → R.Leaf) → (Sample Ω R → ℝ) → ℝ)
    (E : ℝ) (hE : 0 ≤ E)
    (hW : ∀ R pos g, (∀ x, |g x| ≤ 1) →
      (∀ a b, splitDepth R (pos a) (pos b) = splitDepth T (q a) (q b)) → |W R pos g| ≤ E)
    (cs : List C) (U : Finset ι) (loc : ι → S.Leaf) (pos : C → S.Leaf)
    (f : Sample Ω S → ℝ) (hf : ∀ x, |f x| ≤ 1) (hU : U.card ≤ leaves S) :
    |labeledHistory (grid L 0 L)
      (fun R pos g => if ∀ a b, splitDepth R (pos a) (pos b) = splitDepth T (q a) (q b)
        then W R pos g else 0) cs S U loc pos f| ≤
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.branchingCount, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.leaves, OAI.DilutedSpinGlass.PrescribedTree.labeledHistory, OAI.DilutedSpinGlass.PrescribedTree.grid