Chapter H3

import Definitions.Def_ChapterH1
import Mathlib


/-!
# Chapter H3 — Hashimoto SIRK: Duhamel identity and rational-Krylov inclusion (roadmap N13, §0 S7)

This file continues the Hashimoto–Nodera *Shift-invert Rational Krylov (SIRK)*
formalization (source `RiemannProof/Hashimoto.md`), begun in `ChapterH1.lean`
and `ChapterH2.lean`.  It lands two more of the N13 deliverables:

* **H1.3 — the exponential-integrator Duhamel identity (scheme (4)), scalar
  core.** The exact solution of `u' = z·u + g` over `[0,δ]` with constant `g`
  is `u δ = e^{δ z} u₀ + δ·φ₁(δ z)·g`; the load-bearing identity is the Duhamel
  integral `∫₀^δ e^{(δ−s) z} ds = δ·φ₁(δ z)` (`duhamel_scalar`), with the
  forcing-term corollary `duhamel_scalar_smul`.  This is exactly the scalar /
  per-spectral-component reduction (§0 S3) of the operator scheme (4); the `φ₁`
  here is the `ChapterH1.phi` of H1.1/H1.2.
* **H1.7 — the rational-Krylov subspace ⊆ rational functions of `Xₘ` (eq. 11).**
  With the SIRK shift identity `X_j = Y_j · Xₘ` of H1.6 (where
  `Y_j = (1 + h(m−j)·Xₘ)⁻¹`), every SIRK Krylov iterate
  `w_j = X_j ⋯ X_1 v` is a *rational function of the single operator `Xₘ`*
  applied to `v`, i.e. lies in `{ r v | r ∈ 𝒜 }` where `𝒜` is the subalgebra
  generated by `Xₘ` and the resolvent factors `Y_j` (`sirk_krylov_mem_adjoin`).
  This is the mathematically load-bearing inclusion behind the SIRK convergence
  theory (the reverse inclusion — surjectivity onto all of `R_SIRK` — is noted
  in the docstring but not needed for the error bound).

Everything is `sorry`-free and `axiom`-free (only `propext`, `Classical.choice`,
`Quot.sound`); **no `EXTERNAL` hypothesis, no `axiom`**.
-/

open scoped BigOperators
open intervalIntegral

namespace BookProof.ChapterH3

noncomputable section

/-! ## H1.3 — the exponential-integrator Duhamel identity (scalar core) -/





/-! ## H1.7 — the rational-Krylov subspace ⊆ rational functions of `Xₘ` -/

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]

/-- The SIRK Krylov iterates `w_j = X_j ⋯ X_1 v`, defined over `ℕ` with a family
`X : ℕ → Module.End ℂ E` of shift-invert resolvents (`X (j+1)` is the resolvent
at shift `γ_{j+1}`).  `w 0 = v`, `w (j+1) = X (j+1) (w j)`. -/
def sirkKrylov (X : ℕ → Module.End ℂ E) (v : E) : ℕ → E
  | 0 => v
  | (j + 1) => X (j + 1) (sirkKrylov X v j)





/-
**H1.7** (rational-Krylov ⊆ rational functions of `Xₘ`, eq. 11): let `Xm` be the
common shift operator, `Y : ℕ → Module.End ℂ E` the resolvent factors
`Y_j = (1 + h(m−j)·Xₘ)⁻¹`, and suppose every shift-invert resolvent factors as
`X_j = Y_j · Xₘ` (the H1.6 shift identity, `ChapterH1.resolvent_shift_mul`).
Then every SIRK Krylov iterate `w_j` is a *rational function of the single
operator `Xₘ`* applied to `v`: it lies in the image of `v` under the subalgebra
`𝒜 = adjoin ℂ ({Xₘ} ∪ range Y)` of `Module.End ℂ E`.

The reverse inclusion (that the iterates *span* every such rational function of
`Xₘ` applied to `v`) is the surjectivity half of the paper's characterization
and is not needed for the SIRK error bound; only this inclusion is asserted.
-/


end

end BookProof.ChapterH3