# `StronglyContinuousSemigroup.lean` — Informal Summary

> **Source**: [`HilleYosida/StronglyContinuousSemigroup.lean`](../../HilleYosida/StronglyContinuousSemigroup.lean)
> **Generated**: 2026-03-27
> **Note**: Auto-generated by `/lean-summarize`. Re-run to refresh.

## Overview

This file defines strongly continuous one-parameter semigroups ($C_0$-semigroups) on Banach spaces, their infinitesimal generators, and the resolvent operator via the Laplace transform. It proves the forward direction of the Hille-Yosida theorem: for a contraction semigroup, the resolvent $R(\lambda) = \int_0^\infty e^{-\lambda t}\, S(t)\, dt$ satisfies $\lVert R(\lambda) \rVert \le 1/\lambda$, and $(\lambda I - A)\, R(\lambda) = I$.

## Status

**Main result**: Fully proven (0 sorry's)
None --- file is sorry-free.
**Length**: 867 lines, 7 definitions/structures + 13 theorems/lemmas

---

## Key declarations

### `StronglyContinuousSemigroup` (line 97) --- Structure
A family $S(t)$ of bounded linear operators on a Banach space $X$ for $t \ge 0$, satisfying $S(0) = \mathrm{Id}$, $S(s+t) = S(s) \circ S(t)$, and strong continuity at $t = 0$ for each $x \in X$.

### `ContractingSemigroup` (line 111) --- Structure
Extends `StronglyContinuousSemigroup` with $\lVert S(t) \rVert \le 1$ for all $t \ge 0$. Corresponds to growth bound $\omega_0 = 0$.

### `StronglyContinuousSemigroup.strongContAt` (line 249) --- Theorem
Strong continuity at every $t_0 \ge 0$, not just at $0$. Left continuity uses the operator norm bound from `normBoundedOnInterval`; right continuity uses the semigroup property and continuity of $S(t_0)$.

### `StronglyContinuousSemigroup.domain` (line 363) --- Definition
The generator domain $D(A) = \{x : \lim_{t \to 0^+} (S(t)x - x)/t \text{ exists}\}$ as a `Submodule` over $\mathbb{R}$. Closure under addition and scalar multiplication follows from limit laws.

### `StronglyContinuousSemigroup.generatorMap` (line 401) --- Definition
The infinitesimal generator $A : D(A) \to X$, $Ax = \lim_{t \to 0^+} (S(t)x - x)/t$, as a `LinearMap`. Uses `Classical.choose`; linearity from `tendsto_nhds_unique`.

### `ContractingSemigroup.resolvent` (line 493) --- Definition
The resolvent $R(\lambda)\, x = \int_0^\infty e^{-\lambda t}\, S(t)\, x\, dt$ for $\lambda > 0$, constructed via `LinearMap.mkContinuous` with built-in bound $\lVert R(\lambda) \rVert \le 1/\lambda$.

### `ContractingSemigroup.resolventMapsToDomain` (line 746) --- Theorem
$R(\lambda)\, x \in D(A)$ for all $x \in X$. Uses the integral shift trick: $S(h)(R_\lambda x) = e^{\lambda h} \int_{h}^{\infty} f(u)\, du$.

### `ContractingSemigroup.resolventRightInv` (line 765) --- Theorem
$(\lambda I - A)\, R(\lambda)\, x = x$, i.e., the resolvent is the right inverse of $\lambda I - A$.

### `hilleYosidaResolventBound` (line 800) --- Theorem
**Hille-Yosida forward direction.** For a contraction semigroup: $\lVert R(\lambda) \rVert \le 1/\lambda$ for all $\lambda > 0$. Follows immediately from `LinearMap.mkContinuous_norm_le`.

### `StronglyContinuousSemigroup.HasGrowthBound` (line 812) --- Definition
$\lVert S(t) \rVert \le M\, e^{\omega t}$ for all $t \ge 0$, with $M \ge 1$.

### `StronglyContinuousSemigroup.existsGrowthBound` (line 820) --- Theorem
Every $C_0$-semigroup has exponential growth: $\lVert S(t) \rVert \le M\, e^{\omega t}$. Uses the uniform bound on $[0,1]$ from `normBoundedOnUnitInterval` (Banach-Steinhaus) and decomposes $t = \lfloor t \rfloor + \mathrm{frac}(t)$.

---

*This file has **7** definitions/structures and **13** theorems/lemmas (0 with sorry).*