theorem
CommutingRepetition.Resolver.entropy_budget
{A : Type u_1}
[CStarAlgebra A]
[PartialOrder A]
[StarOrderedRing A]
{I : Type}
[Fintype I]
[DecidableEq I]
(Fs : I → A)
(hF0 : ∀ (i : I), 0 ≤ Fs i)
(hF1 : ∀ (i : I), Fs i ≤ 1)
(ω : A →ₗ[ℝ] ℝ)
(hmono : ∀ {a b : A}, a ≤ b → ω a ≤ ω b)
(hm1 : ω 1 ≤ 1)
{V : Type u_2}
[NormedAddCommGroup V]
(Φ : I → V)
(hinc :
∀ (i i' : I),
‖Φ i - Φ i'‖ ^ 2 = ω (kern (Fs i) (Fs i) - kern (Fs i) (Fs i') - kern (Fs i') (Fs i) + kern (Fs i') (Fs i')))
{steps : ℕ}
{Ω : Type}
[Fintype Ω]
(law : Ω → ℝ)
(hlaw : ∀ (ω : Ω), 0 ≤ law ω)
(hsum : ∑ ω : Ω, law ω = 1)
(idx : Fin (steps + 1) → Ω → I)
(hidx0 : ∀ (ω ω' : Ω), idx 0 ω = idx 0 ω')
(htower :
∀ (s : Fin steps) (i : I),
∑ ω : Ω, (if idx s.castSucc ω = i then law ω else 0) • Fs (idx s.succ ω) = (∑ ω : Ω, if idx s.castSucc ω = i then law ω else 0) • Fs i)
(ω₀ : Ω)
:
The telescoped entropy budget.