# `GenerationTheorem.lean` — Informal Summary

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

## Overview

This file states the **converse direction of the Hille-Yosida theorem** as axioms. While the forward direction (semigroup implies resolvent bound) is fully proved in `StronglyContinuousSemigroup.lean`, the converse (operator generates a semigroup) requires the Yosida approximation and is stated here for use by downstream projects. It also defines dissipative operators and the Lumer-Phillips characterization.

## Status

**Main result**: Not yet proven (2 axioms)
- `StronglyContinuousSemigroup.domain_isDense` (axiom, line 53)
- `hilleYosidaGeneration` (axiom, line 98)

**Length**: 109 lines, 2 definitions/structures + 2 axioms

---

## Key declarations

### `StronglyContinuousSemigroup.domain_isDense` (line 53) --- Axiom
The generator domain $D(A)$ is dense in $X$. The proof (not yet formalized) uses "smoothed" elements $x_t = (1/t) \int_0^t S(s)x\, ds \in D(A)$ which converge to $x$ as $t \to 0$.

Ref: [EN] Thm. II.1.4.

### `DenseLinearOperator` (line 65) --- Structure
A densely defined linear operator $A$ on a Banach space $X$: a submodule `domain`, a linear map `op : domain -> X`, and a proof that `domain` is dense.

### `DenseLinearOperator.IsDissipative` (line 77) --- Definition
An operator $A$ is dissipative if $\lVert (\lambda I - A)x \rVert \ge \lambda \lVert x \rVert$ for all $\lambda > 0$ and $x \in D(A)$.

Ref: [EN] Def. II.3.13.

### `hilleYosidaGeneration` (line 98) --- Axiom
**Hille-Yosida generation theorem** (contraction case, converse). A densely defined, dissipative operator $A$ with $\operatorname{rg}(\lambda_0 - A) = X$ for some $\lambda_0 > 0$ generates a contraction semigroup $S$ such that the generator of $S$ extends $A$.

This is the Lumer-Phillips theorem ([EN] Thm. II.3.15). The proof (to be formalized) constructs the semigroup via the Yosida approximation $A_\lambda = \lambda^2 R(\lambda, A) - \lambda I$ and shows $e^{t A_\lambda}$ converges strongly as $\lambda \to \infty$.

Ref: [EN] Thm. II.3.5, Cor. II.3.6, Thm. II.3.15; [Linares] Thm. 6.

---

*This file has **2** definitions/structures and **2** axioms (both unproved).*