Theorems · Definition · functional analysis

ContinuousLinearMap.lpPairing

{α : Type u_1} →
  {𝕜 : Type u_2} →
    {E : Type u_3} →
      {F : Type u_4} →
        {G : Type u_5} →
          {m : MeasurableSpace α} →
            (μ : MeasureTheory.Measure α) →
              (p q : ENNReal) →
                [inst : NontriviallyNormedField 𝕜] →
                  [inst_1 : NormedAddCommGroup E] →
                    [inst_2 : NormedAddCommGroup F] →
                      [inst_3 : NormedAddCommGroup G] →
                        [inst_4 : NormedSpace 𝕜 E] →
                          [inst_5 : NormedSpace 𝕜 F] →
                            [inst_6 : NormedSpace 𝕜 G] →
                              [inst_7 : Fact (1 ≤ p)] →
                                [inst_8 : Fact (1 ≤ q)] →
                                  [p.HolderConjugate q] →
                                    [inst_10 : NormedSpace ℝ G] →
                                      [SMulCommClass ℝ 𝕜 G] →
                                        [CompleteSpace G] →
                                          (E →L[𝕜] F →L[𝕜] G) →
                                            ↥(MeasureTheory.Lp E p μ) →L[𝕜] ↥(MeasureTheory.Lp F q μ) →L[𝕜] G

The natural pairing between Lp E p μ and Lp F q μ (for Hölder conjugate p q : ℝ≥0∞) with values in a space G induced by a bilinear map B : E →L[𝕜] F →L[𝕜] G. This is given by ∫ x, B (f x) (g x) ∂μ. In the special case when B := (NormedSpace.inclusionInDoubleDual 𝕜 E).flip, which is definitionally the same as B := ContinuousLinearMap.id 𝕜 (E →L[𝕜] 𝕜), this is the natural map Lp (StrongDual 𝕜 E) p μ →L[𝕜] StrongDual 𝕜 (Lp E q μ).

Defined in

Mathlib.MeasureTheory.Function.Holder

Cited by

3 results in Mathlib

Foundations

Depth 241 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedAddCommGroupNormedAddCommGroupNormedSpaceNormedSpaceNormedSpaceFactFactENNReal.HolderConjugateNormedSpaceSMulCommClassCompleteSpace