Finite-basis reconstruction in Lᵖ #
An Lᵖ function with finite-dimensional target is the sum of its scalar coordinate functions
multiplied by the basis vectors. This transports Module.Basis.sum_repr through
ContinuousLinearMap.compLpL and permits coordinatewise arguments about vector-valued operators.
In particular, an operator into Lᵖ with finite-dimensional target is compact as soon as each of
its scalar projections is compact
(TauCeti.isCompactOperator_of_forall_isCompactOperator_compLpL_comp).
theorem
TauCeti.eq_sum_basis_compLpL
{α : Type u_1}
{𝕜 : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[MeasurableSpace α]
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[FiniteDimensional 𝕜 F]
[Fintype ι]
{p : ENNReal}
[Fact (1 ≤ p)]
{μ : MeasureTheory.Measure α}
(b : Module.Basis ι 𝕜 F)
(f : ↥(MeasureTheory.Lp F p μ))
:
f = ∑ i : ι,
(ContinuousLinearMap.compLpL p μ (ContinuousLinearMap.toSpanSingleton 𝕜 (b i)))
((ContinuousLinearMap.compLpL p μ (LinearMap.toContinuousLinearMap (b.coord i))) f)
Reconstruct an Lᵖ function from its coordinates in a finite basis.
theorem
TauCeti.isCompactOperator_of_forall_isCompactOperator_compLpL_comp
{α : Type u_1}
{𝕜 : Type u_2}
{F : Type u_3}
[MeasurableSpace α]
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[FiniteDimensional 𝕜 F]
{p : ENNReal}
[Fact (1 ≤ p)]
{μ : MeasureTheory.Measure α}
{Y : Type u_5}
[SeminormedAddCommGroup Y]
[NormedSpace 𝕜 Y]
(T : Y →L[𝕜] ↥(MeasureTheory.Lp F p μ))
(h : ∀ (ℓ : F →L[𝕜] 𝕜), IsCompactOperator ⇑(ContinuousLinearMap.compLpL p μ ℓ ∘SL T))
:
An operator into Lᵖ with finite-dimensional target is compact as soon as its composition
with every scalar projection ℓ.compLpL p μ is compact.