Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 5 research declarations. Search 10,000 more complete Mathlib declarations.
5 results
Clear filtersBareFunction.ae_eq_of_tendsto_eLpNorm_sub
Plain-language statement
Lp limit uniqueness: if f_n → g₁ and f_n → g₂ in eLpNorm, then g₁ =ᵐ g₂.
Source project: DeGiorgi
Person-level attribution pending.
BareFunction.eLpNorm_pi_le_sum_component
Plain-language statement
Vector eLpNorm ≤ sum of component eLpNorms for Pi-valued functions. Uses eLpNorm_mono_real for the pointwise bound together with eLpNorm_sum_le for ℝ-valued functions, avoiding Pi instance synthesis.
Source project: DeGiorgi
Person-level attribution pending.
BareFunction.memLp_of_tendsto_eLpNorm
Plain-language statement
If f n → g in eLpNorm and each f n ∈ Lp, then g ∈ Lp, provided g is AEStronglyMeasurable. Avoids the Lp type entirely. The key observation: eLpNorm (f n - g) → 0 means eLpNorm (f N - g) < 1 for some N. Then eLpNorm g ≤ eLpNorm (f N - g) + eLpNorm (f N) < ∞.
Source project: DeGiorgi
Person-level attribution pending.
BareFunction.scalar_cauchy_to_limit
Plain-language statement
Scalar Cauchy → limit. Generic over codomain E and domain α.
Source project: DeGiorgi
Person-level attribution pending.
BareFunction.tendsto_eLpNorm_pi_component
Plain-language statement
Vector eLpNorm convergence → component eLpNorm convergence. Uses eLpNorm_pi_component_le via an explicit function equality to avoid expensive defeq checks.
Source project: DeGiorgi
Person-level attribution pending.