`BookProof.BrstLeakage.leakageIter_succ` (B : ℕ → E →L[ℂ] E) (τ : ℝ) (x : E) (n : ℕ) : leakageIter B τ x (n + 1) = flow (B n) τ (leakageIter B τ x n)
ProvedBookProof.BrstLeakage.leakageIter_succtheoremstimepiece
Prove the following Lean 4 theorem from ChapterBrstTruncationLeakage.
BookProof.BrstLeakage.leakageIter_succ (B : ℕ → E →L[ℂ] E) (τ : ℝ) (x : E) (n : ℕ) : leakageIter B τ x (n + 1) = flow (B n) τ (leakageIter B τ x n)
Formalization note: Lean 4 identifier BookProof.BrstLeakage.leakageIter_succ.
Preamble
-- Generated from ChapterBrstTruncationLeakage.lean — theorem BookProof.BrstLeakage.leakageIter_succ
import Mathlib
import Definitions.Def_ChapterBrstTruncationLeakage
open BookProof.BrstLeakage
open NormedSpace
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]Formal statement
theorem BookProof.BrstLeakage.leakageIter_succ (B : ℕ → E →L[ℂ] E) (τ : ℝ) (x : E) (n : ℕ) :
leakageIter B τ x (n + 1) = flow (B n) τ (leakageIter B τ x n) := by sorry