Convergence of Hölder bilinear products #
Continuous bilinear maps send convergent pairs of Lp classes at Hölder exponents to convergent
products. On finite-measure subsets, this gives convergence in the L¹ distance of arbitrary
almost-everywhere representatives.
theorem
ContinuousLinearMap.holderL_ae_eq_of_measure_le
{E : Type u_1}
{F : Type u_2}
{G : Type u_3}
{H : Type u_4}
[MeasurableSpace E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
{μ : MeasureTheory.Measure E}
{p q r : ENNReal}
[Fact (1 ≤ p)]
[Fact (1 ≤ q)]
[Fact (1 ≤ r)]
[p.HolderTriple q r]
(B : F →L[ℝ] G →L[ℝ] H)
{ν : MeasureTheory.Measure E}
(hν : ν ≤ μ)
(a : ↥(MeasureTheory.Lp F p μ))
(c : ↥(MeasureTheory.Lp G q μ))
{f : E → F}
{g : E → G}
(ha : ↑↑a =ᵐ[ν] f)
(hc : ↑↑c =ᵐ[ν] g)
:
↑↑(((holderL μ p q r B) a) c) =ᵐ[ν] fun (x : E) => (B (f x)) (g x)
A Hölder product agrees with the bilinear product of chosen representatives for any dominated measure.
theorem
TauCeti.tendsto_setLIntegral_enorm_bilin_sub
{E : Type u_1}
{F : Type u_2}
{G : Type u_3}
{H : Type u_4}
{ι : Type u_5}
[MeasurableSpace E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
{μ : MeasureTheory.Measure E}
{p q r : ENNReal}
[Fact (1 ≤ p)]
[Fact (1 ≤ q)]
[Fact (1 ≤ r)]
[p.HolderTriple q r]
(B : F →L[ℝ] G →L[ℝ] H)
{W : Set E}
(hW : μ W < ⊤)
{l : Filter ι}
{A : ι → ↥(MeasureTheory.Lp F p μ)}
{A₀ : ↥(MeasureTheory.Lp F p μ)}
{C : ι → ↥(MeasureTheory.Lp G q μ)}
{C₀ : ↥(MeasureTheory.Lp G q μ)}
(hA : Filter.Tendsto A l (nhds A₀))
(hC : Filter.Tendsto C l (nhds C₀))
{a : ι → E → F}
{a₀ : E → F}
{c : ι → E → G}
{c₀ : E → G}
(ha : ∀ (n : ι), ↑↑(A n) =ᵐ[μ] a n)
(ha₀ : ↑↑A₀ =ᵐ[μ.restrict W] a₀)
(hc : ∀ (n : ι), ↑↑(C n) =ᵐ[μ] c n)
(hc₀ : ↑↑C₀ =ᵐ[μ.restrict W] c₀)
:
Hölder bilinear products of convergent Lp classes converge in L¹ on finite-measure sets,
with the limits and approximants stated for arbitrary almost-everywhere representatives.