English
The almost-everywhere equality holds: the value of the composed map equals applying L to the value of f, a.e.
Русский
Почти повсеместно выполняется равенство: значение композиции равно применению L к значению f.
LaTeX
$$$L.compLpL\\, f =^{\\mathrm{ae}} a\\mapsto L\\bigl(f(a)\\bigr).$$$
Lean4
/-- Composing `f : Lp E p μ` with `L : E →L[𝕜] F`, seen as a continuous `𝕜`-linear map on
`Lp E p μ`. See also the similar
* `LinearMap.compLeft` for functions,
* `ContinuousLinearMap.compLeftContinuous` for continuous functions,
* `ContinuousLinearMap.compLeftContinuousBounded` for bounded continuous functions,
* `ContinuousLinearMap.compLeftContinuousCompact` for continuous functions on compact spaces.
-/
def compLpL [Fact (1 ≤ p)] (L : E →SL[σ] F) : Lp E p μ →SL[σ] Lp F p μ :=
LinearMap.mkContinuous (L.compLpₗ p μ) ‖L‖ L.norm_compLp_le
