Banach space theory

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremPietsch domination theorem #

For 1 ≤ p < ∞ and C ≥ 0, an operator satisfies πₚ(T) ≤ C if and only if there is a regular Borel probability measure ν on the weak-star compact dual unit ball with ‖T x‖ ≤ C (∫ |f x|ᵖ dν(f))^(1/p) for all x.

ContinuousLinearMap.summingENorm_le_ofReal_iff_exists_isProbabilityMeasure.{u_1, u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E]
  [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal} [Fact (1 ≤ p)]
  [MeasurableSpace (WeakDual 𝕜 E)] [BorelSpace (WeakDual 𝕜 E)] (hp : p ≠ ⊤) {T : E →L[𝕜] F} {C : ℝ}
  (hC : 0 ≤ C) :
  ContinuousLinearMap.summingENorm p T ≤ ENNReal.ofReal C ↔
    ∃ ν,
      MeasureTheory.IsProbabilityMeasure ν ∧
        ν.Regular ∧
          ∀ (x : E),
            ‖T x‖ ≤
              C *
                (∫ (f : ↑(⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall 0 1)),
                    ‖↑f x‖ ^ p.toReal ∂ν) ^
                  (1 / p.toReal)

Lean

Formalized in Tau Ceti as ContinuousLinearMap.summingENorm_le_ofReal_iff_exists_isProbabilityMeasure.

Sources

LeanContinuousLinearMap.summingENorm_le_ofReal_iff_exists_isProbabilityMeasure

Uses 1 · Used by 1

Proof usesRiesz–Markov–Kakutani on a compact Hausdorff space

Used byPietsch factorization through the closure of the canonical image

TheoremPietsch factorization through the closure of the canonical image #

for a Banach space F, 1 ≤ p < ∞ and C ≥ 0, πₚ(T) ≤ C iff there are a regular Borel probability measure ν on the weak-star compact dual unit ball and an operator S of norm at most C on the closure of range jₚ in Lᵖ(ν) such that T = S ∘ jₚ.

ContinuousLinearMap.summingENorm_le_ofReal_iff_exists_eq_comp_codRestrict_topologicalClosure.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E]
  [NormedSpace 𝕜 E] [MeasurableSpace (WeakDual 𝕜 E)] [BorelSpace (WeakDual 𝕜 E)] {p : ENNReal}
  [Fact (1 ≤ p)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (hp : p ≠ ⊤)
  {T : E →L[𝕜] F} {C : ℝ} (hC : 0 ≤ C) :
  ContinuousLinearMap.summingENorm p T ≤ ENNReal.ofReal C ↔
    ∃ ν,
      ∃ (x : MeasureTheory.IsProbabilityMeasure ν),
        ν.Regular ∧
          ∃ S,
            ‖S‖ ≤ C ∧
              T =
                S ∘SL
                  (WeakDual.evalLp p ν).codRestrict
                    (↑(WeakDual.evalLp p ν)).range.topologicalClosure ⋯

Lean

Formalized in Tau Ceti as ContinuousLinearMap.summingENorm_le_ofReal_iff_exists_eq_comp_codRestrict_topologicalClosure.

Sources

LeanContinuousLinearMap.summingENorm_le_ofReal_iff_exists_eq_comp_codRestrict_topologicalClosure

Uses 1

Proof usesPietsch domination theorem

TheoremClosed-range theorem #

A bounded operator between Banach spaces has closed range if and only if its adjoint has closed range.

ContinuousLinearMap.isClosed_range_precomp_iff.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) :
  IsClosed ↑(↑(ContinuousLinearMap.precomp 𝕜 T)).range ↔ IsClosed ↑(↑T).range

Lean

Formalized in Tau Ceti as ContinuousLinearMap.isClosed_range_precomp_iff.

Other forms

Closed-range theorem, range of the adjoint. Formalized in Tau Ceti as ContinuousLinearMap.range_precomp_eq_orthogonalBilin_ker.

ContinuousLinearMap.range_precomp_eq_orthogonalBilin_ker.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F]
  [NormedSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) (hT : IsClosed ↑(↑T).range) :
  (↑(ContinuousLinearMap.precomp 𝕜 T)).range =
    Submodule.orthogonalBilin (topDualPairing 𝕜 E).flip (↑T).ker

Closed-range theorem, reverse implication. Formalized in Tau Ceti as ContinuousLinearMap.isClosed_range_of_isClosed_range_precomp.

ContinuousLinearMap.isClosed_range_of_isClosed_range_precomp.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
  [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F)
  (h : IsClosed ↑(↑(ContinuousLinearMap.precomp 𝕜 T)).range) : IsClosed ↑(↑T).range

Sources

LeanContinuousLinearMap.isClosed_range_precomp_iff · ContinuousLinearMap.range_precomp_eq_orthogonalBilin_ker · ContinuousLinearMap.isClosed_range_of_isClosed_range_precomp

Uses 1

Proof usesBanach's lemma

TheoremThe Bishop–Phelps theorem #

The continuous linear functionals on a Banach space which attain their norm on the closed unit ball are norm dense in the dual.

TauCeti.dense_setOf_exists_norm_apply_eq_norm.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] :
  Dense {g | ∃ x, ‖x‖ ≤ 1 ∧ ‖g x‖ = ‖g‖}

Lean

Formalized in Tau Ceti as TauCeti.dense_setOf_exists_norm_apply_eq_norm.

Other forms

The Bishop–Phelps theorem for support functionals. Formalized in Tau Ceti as Convex.dense_setOf_ne_zero_isMaxOn_re.

Convex.dense_setOf_ne_zero_isMaxOn_re.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E] {C : Set E}
  [Nontrivial E] (hconv : Convex ℝ C) (hC : IsComplete C) (hb : Bornology.IsBounded C)
  (hne : C.Nonempty) : Dense {g | g ≠ 0 ∧ ∃ x ∈ C, IsMaxOn (fun y => RCLike.re (g y)) C x}

The Bishop–Phelps theorem for support functionals, in Phelps' general form. Formalized in Tau Ceti as Convex.mem_closure_setOf_ne_zero_isMaxOn_re_of_bddAbove.

Convex.mem_closure_setOf_ne_zero_isMaxOn_re_of_bddAbove.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2}
  [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E]
  {C : Set E} (hconv : Convex ℝ C) (hC : IsComplete C) (hne : C.Nonempty) {f : StrongDual 𝕜 E}
  (hf : f ≠ 0) (hbdd : BddAbove ((fun y => RCLike.re (f y)) '' C)) :
  f ∈ closure {g | g ≠ 0 ∧ ∃ x ∈ C, IsMaxOn (fun y => RCLike.re (g y)) C x}

The Bishop–Phelps theorem for support points. Formalized in Tau Ceti as Convex.frontier_subset_closure_setOf_isMaxOn_re.

Convex.frontier_subset_closure_setOf_isMaxOn_re.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E] {C : Set E}
  (hconv : Convex ℝ C) (hC : IsComplete C) :
  frontier C ⊆ closure {x | x ∈ C ∧ ∃ g, g ≠ 0 ∧ IsMaxOn (fun y => RCLike.re (g y)) C x}

Sources

LeanTauCeti.dense_setOf_exists_norm_apply_eq_norm · Convex.dense_setOf_ne_zero_isMaxOn_re · Convex.mem_closure_setOf_ne_zero_isMaxOn_re_of_bddAbove · Convex.frontier_subset_closure_setOf_isMaxOn_re

Uses 2

Proof usesThe Bishop–Phelps lemma · Bishop–Phelps support lemma

TheoremMilman–Pettis theorem #

A uniformly convex Banach space is reflexive: its canonical map into the continuous bidual is surjective.

TauCeti.surjective_inclusionInDoubleDual_of_uniformConvexSpace.{u_1, u_2} {𝕜 : Type u_1}
  {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [UniformConvexSpace E]
  [CompleteSpace E] : Function.Surjective ⇑(NormedSpace.inclusionInDoubleDual 𝕜 E)

Lean

Formalized in Tau Ceti as TauCeti.surjective_inclusionInDoubleDual_of_uniformConvexSpace.

Sources

LeanTauCeti.surjective_inclusionInDoubleDual_of_uniformConvexSpace

Uses 1 · Used by 1

Proof usesGoldstine's theorem

Used byDunford–Pettis theorem

TheoremClarkson's inequality #

For 2 ≤ p < ∞ and f g : Lp E p μ, where the norm of E satisfies the parallelogram identity, ‖f + g‖ ^ p + ‖f - g‖ ^ p ≤ 2 ^ (p - 1) * (‖f‖ ^ p + ‖g‖ ^ p).

MeasureTheory.Lp.norm_add_rpow_add_norm_sub_rpow_le.{u_1, u_2} {α : Type u_1} {E : Type u_2}
  {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {p : ENNReal}
  [InnerProductSpaceable E] (hp : 2 ≤ p) (hp_top : p ≠ ⊤) (f g : ↥(MeasureTheory.Lp E p μ)) :
  ‖f + g‖ ^ p.toReal + ‖f - g‖ ^ p.toReal ≤ 2 ^ (p.toReal - 1) * (‖f‖ ^ p.toReal + ‖g‖ ^ p.toReal)

Lean

Formalized in Tau Ceti as MeasureTheory.Lp.norm_add_rpow_add_norm_sub_rpow_le.

Sources

LeanMeasureTheory.Lp.norm_add_rpow_add_norm_sub_rpow_le

Uses 1

Proof usesThe pointwise Clarkson inequality

TheoremJames's basis criterion #

A Banach space with a Schauder basis is reflexive if and only if that basis is shrinking and boundedly complete.

SchauderBasis.surjective_inclusionInDoubleDual_iff.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2}
  [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (b : SchauderBasis 𝕜 E) [CompleteSpace E] :
  Function.Surjective ⇑(NormedSpace.inclusionInDoubleDual 𝕜 E) ↔
    b.IsShrinking ∧ b.IsBoundedlyComplete

Lean

Formalized in Tau Ceti as SchauderBasis.surjective_inclusionInDoubleDual_iff.

Sources

LeanSchauderBasis.surjective_inclusionInDoubleDual_iff

AbbreviationTauCeti.AbsolutelySumming #

The operator ideal Πₚ(E, F) of absolutely p-summing operators, normed by the p-summing norm πₚ. It is a Banach space when F is complete, and its inclusion OperatorGauge.Carrier.toContinuousLinearMapL into the bounded operators is a contraction.

TauCeti.AbsolutelySumming.{u_1, u_2, u_3} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (p : ENNReal)
  [Fact (1 ≤ p)] (E : Type u_2) (F : Type u_3) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
  [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : Type (max u_2 u_3)

Lean

Formalized in Tau Ceti as TauCeti.AbsolutelySumming.

Sources

LeanTauCeti.AbsolutelySumming

DefinitionTauCeti.HasApproximationProperty #

The identity can be approximated uniformly on every norm-compact set by bounded operators with finite-dimensional range.

TauCeti.HasApproximationProperty.{u_1, u_2} (𝕜 : Type u_1) (E : Type u_2)
  [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Prop

Lean

Formalized in Tau Ceti as TauCeti.HasApproximationProperty.

Sources

LeanTauCeti.HasApproximationProperty

StructureTauCeti.ProjectiveTensor #

The algebraic tensor product E ⊗[𝕜] F carrying the projective seminorm.

This wrapper distinguishes the projective seminorm from other norms on the same algebraic tensor product, such as the injective norm or the Hilbert-space norm of inner product spaces.

TauCeti.ProjectiveTensor.{u_1, u_2, u_3} (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3)
  [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F]
  [NormedSpace 𝕜 F] : Type (max u_2 u_3)

Lean

Formalized in Tau Ceti as TauCeti.ProjectiveTensor.

Sources

LeanTauCeti.ProjectiveTensor

StructureTauCeti.InjectiveTensor #

The algebraic tensor product E ⊗[𝕜] F carrying the injective seminorm.

This wrapper distinguishes the injective seminorm from other norms on the same algebraic tensor product, such as the projective norm or the Hilbert-space norm of inner product spaces.

TauCeti.InjectiveTensor.{u_1, u_2, u_3} (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3)
  [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
  [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : Type (max u_2 u_3)

Lean

Formalized in Tau Ceti as TauCeti.InjectiveTensor.

Sources

LeanTauCeti.InjectiveTensor

TheoremThe Bishop–Phelps lemma #

Let 0 ≤ k < 1 and f ≠ 0. If the real part of h is positive on the open cone {x | k * ‖f‖ * ‖x‖ < re (f x)}, then some positive real multiple of h lies within k * ‖f‖ of f.

StrongDual.exists_pos_norm_sub_ofReal_smul_le.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f h : StrongDual 𝕜 E) {k : ℝ} (hk₀ : 0 ≤ k)
  (hk₁ : k < 1) (hf : f ≠ 0)
  (hpos : ∀ (x : E), k * ‖f‖ * ‖x‖ < RCLike.re (f x) → 0 < RCLike.re (h x)) :
  ∃ c, 0 < c ∧ ‖f - ↑c • h‖ ≤ k * ‖f‖

Lean

Formalized in Tau Ceti as StrongDual.exists_pos_norm_sub_ofReal_smul_le.

Sources

LeanStrongDual.exists_pos_norm_sub_ofReal_smul_le

Used by 1

Used byThe Bishop–Phelps theorem

TheoremBishop–Phelps support lemma #

Let C be a complete convex subset of a normed space, let f be a nonzero functional whose real part is bounded above on C, and let 0 < k < 1. From every z ∈ C one reaches a point x ∈ C with k * ‖f‖ * ‖x - z‖ ≤ re (f (x - z)) at which C has a support functional h, nonzero and with real part positive on the open cone {w | k * ‖f‖ * ‖w‖ < re (f w)}.

Convex.exists_isMaxOn_re_of_bddAbove.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E] {C : Set E}
  (hconv : Convex ℝ C) (hC : IsComplete C) {f : StrongDual 𝕜 E} (hf : f ≠ 0)
  (hbdd : BddAbove ((fun y => RCLike.re (f y)) '' C)) {k : ℝ} (hk₀ : 0 < k) (hk₁ : k < 1) {z : E}
  (hz : z ∈ C) :
  ∃ x ∈ C,
    k * ‖f‖ * ‖x - z‖ ≤ RCLike.re (f (x - z)) ∧
      ∃ h,
        h ≠ 0 ∧
          IsMaxOn (fun y => RCLike.re (h y)) C x ∧
            ∀ (w : E), k * ‖f‖ * ‖w‖ < RCLike.re (f w) → 0 < RCLike.re (h w)

Lean

Formalized in Tau Ceti as Convex.exists_isMaxOn_re_of_bddAbove.

Sources

LeanConvex.exists_isMaxOn_re_of_bddAbove

Uses 1 · Used by 1

Proof usesEkeland's variational principle

Used byThe Bishop–Phelps theorem

TheoremGoldstine's theorem #

The weak-star closure of the image of the closed ball closedBall x r under the canonical embedding into the bidual is the closed ball of radius r about the image of x.

NormedSpace.closure_image_inclusionInDoubleDualWeak_closedBall.{u_1, u_2} (𝕜 : Type u_1)
  (E : Type u_2) [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (r : ℝ) :
  closure
      (⇑(NormedSpace.inclusionInDoubleDualWeak 𝕜 E) ''
        ⇑(toWeakSpace 𝕜 E) '' Metric.closedBall x r) =
    ⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall ((NormedSpace.inclusionInDoubleDual 𝕜 E) x) r

Lean

Formalized in Tau Ceti as NormedSpace.closure_image_inclusionInDoubleDualWeak_closedBall.

Other forms

Goldstine's theorem, unit-ball form. Formalized in Tau Ceti as NormedSpace.closure_image_inclusionInDoubleDualWeak_closedBall_zero_one.

NormedSpace.closure_image_inclusionInDoubleDualWeak_closedBall_zero_one.{u_1, u_2} (𝕜 : Type u_1)
  (E : Type u_2) [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
  closure
      (⇑(NormedSpace.inclusionInDoubleDualWeak 𝕜 E) ''
        ⇑(toWeakSpace 𝕜 E) '' Metric.closedBall 0 1) =
    ⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall 0 1

Sources

LeanNormedSpace.closure_image_inclusionInDoubleDualWeak_closedBall · NormedSpace.closure_image_inclusionInDoubleDualWeak_closedBall_zero_one

Used by 3

Used byHelly's lemma · Milman–Pettis theorem · Gantmacher's criterion

TheoremGrothendieck's theorem #

Every bounded operator T from L¹(μ) into an inner product space over an RCLike field is absolutely 1-summing, with π₁(T) ≤ 16 ‖T‖. Over ℝ, ContinuousLinearMap.summingENorm_one_le_ofReal_eight_mul_norm gives the constant 8.

ContinuousLinearMap.summingENorm_one_le_ofReal_sixteen_mul_norm.{u_1, u_2, u_3} {α : Type u_1}
  {𝕜 : Type u_2} {H : Type u_3} [RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (T : ↥(MeasureTheory.Lp 𝕜 1 μ) →L[𝕜] H) :
  ContinuousLinearMap.summingENorm 1 T ≤ ENNReal.ofReal (16 * ‖T‖)

Lean

Formalized in Tau Ceti as ContinuousLinearMap.summingENorm_one_le_ofReal_sixteen_mul_norm.

Other forms

Grothendieck's theorem over ℝ. Formalized in Tau Ceti as ContinuousLinearMap.summingENorm_one_le_ofReal_eight_mul_norm.

ContinuousLinearMap.summingENorm_one_le_ofReal_eight_mul_norm.{u_1, u_4} {α : Type u_1}
  {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {H : Type u_4} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (T : ↥(MeasureTheory.Lp ℝ 1 μ) →L[ℝ] H) :
  ContinuousLinearMap.summingENorm 1 T ≤ ENNReal.ofReal (8 * ‖T‖)

Sources

LeanContinuousLinearMap.summingENorm_one_le_ofReal_sixteen_mul_norm · ContinuousLinearMap.summingENorm_one_le_ofReal_eight_mul_norm

Uses 1

Proof usesGrothendieck's inequality over the reals, with constant κ_ℝ = 8

TheoremHelly's criterion #

Let f i be finitely many continuous linear functionals on E, let c i be scalars and let 0 ≤ M. For every ε > 0 some x : E with ‖x‖ < M + ε satisfies f i x = c i for every i if and only if ‖∑ i, a i * c i‖ ≤ M * ‖∑ i, a i • f i‖ for all scalars a i.

TauCeti.exists_norm_lt_and_forall_apply_eq_iff.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2}
  [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {ι : Type u_3} [Fintype ι]
  (f : ι → StrongDual 𝕜 E) (c : ι → 𝕜) {M : ℝ} (hM : 0 ≤ M) :
  (∀ ε > 0, ∃ x, ‖x‖ < M + ε ∧ ∀ (i : ι), (f i) x = c i) ↔
    ∀ (a : ι → 𝕜), ‖∑ i, a i * c i‖ ≤ M * ‖∑ i, a i • f i‖

Lean

Formalized in Tau Ceti as TauCeti.exists_norm_lt_and_forall_apply_eq_iff.

Sources

LeanTauCeti.exists_norm_lt_and_forall_apply_eq_iff

Uses 1

Proof usesHelly's lemma

TheoremHelly's lemma #

For an element φ of the bidual of E, finitely many continuous linear functionals f i on E and ε > 0, some x : E with ‖x‖ < ‖φ‖ + ε satisfies f i x = φ (f i) for every i.

StrongDual.exists_norm_lt_and_forall_apply_eq.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2}
  [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (φ : StrongDual 𝕜 (StrongDual 𝕜 E))
  {ι : Type u_3} [Finite ι] (f : ι → StrongDual 𝕜 E) {ε : ℝ} (hε : 0 < ε) :
  ∃ x, ‖x‖ < ‖φ‖ + ε ∧ ∀ (i : ι), (f i) x = φ (f i)

Lean

Formalized in Tau Ceti as StrongDual.exists_norm_lt_and_forall_apply_eq.

Other forms

Helly's lemma for a finite-dimensional subspace W of the dual. Formalized in Tau Ceti as StrongDual.exists_norm_lt_and_forall_mem_apply_eq.

StrongDual.exists_norm_lt_and_forall_mem_apply_eq.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2}
  [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (φ : StrongDual 𝕜 (StrongDual 𝕜 E))
  (W : Submodule 𝕜 (StrongDual 𝕜 E)) [FiniteDimensional 𝕜 ↥W] {ε : ℝ} (hε : 0 < ε) :
  ∃ x, ‖x‖ < ‖φ‖ + ε ∧ ∀ f ∈ W, f x = φ f

Helly's lemma, coordinatewise. Formalized in Tau Ceti as StrongDual.norm_sum_apply_comp_single_le.

StrongDual.norm_sum_apply_comp_single_le.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {κ : Type u_3} [Fintype κ] [DecidableEq κ]
  (f : StrongDual 𝕜 (κ → E)) (hf : ‖f‖ ≤ 1) (z : κ → StrongDual 𝕜 (StrongDual 𝕜 E))
  (hz : ∀ (i : κ), ‖z i‖ ≤ 1) : ‖∑ i, (z i) (f ∘SL ContinuousLinearMap.single 𝕜 (fun x => E) i)‖ ≤ 1

Sources

LeanStrongDual.exists_norm_lt_and_forall_apply_eq · StrongDual.exists_norm_lt_and_forall_mem_apply_eq · StrongDual.norm_sum_apply_comp_single_le

Uses 1 · Used by 1

Proof usesGoldstine's theorem

Used byHelly's criterion

TheoremKrein–Šmulian theorem #

A convex subset of the dual of a Banach space is weak-star closed if and only if its intersection with every closed ball centred at zero is weak-star closed.

Convex.isClosed_iff_forall_isClosed_inter_closedBall.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2}
  [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {C : Set (WeakDual 𝕜 E)}
  (hC : Convex ℝ C) :
  IsClosed C ↔ ∀ (r : ℝ), IsClosed (C ∩ ⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall 0 r)

Lean

Formalized in Tau Ceti as Convex.isClosed_iff_forall_isClosed_inter_closedBall.

Sources

LeanConvex.isClosed_iff_forall_isClosed_inter_closedBall

Uses 1 · Used by 1

Proof usesSeparation lemma of the Krein–Šmulian theorem

Used byKrein–Šmulian theorem for subspaces

TheoremKrein–Šmulian theorem for subspaces #

A subspace of the dual of a Banach space is weak-star closed if and only if its intersection with the closed unit ball is weak-star closed.

Submodule.isClosed_iff_isClosed_inter_closedBall_zero_one.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2}
  [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
  (G : Submodule 𝕜 (WeakDual 𝕜 E)) :
  IsClosed ↑G ↔ IsClosed (↑G ∩ ⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall 0 1)

Lean

Formalized in Tau Ceti as Submodule.isClosed_iff_isClosed_inter_closedBall_zero_one.

Sources

LeanSubmodule.isClosed_iff_isClosed_inter_closedBall_zero_one

Uses 1

Proof usesKrein–Šmulian theorem

TheoremSeparation lemma of the Krein–Šmulian theorem #

Let C be a convex set of functionals on a Banach space whose intersection with every closed ball centred at zero is weak-star closed. If every element of C has norm greater than some r > 0, then evaluation at a single point x separates C from zero: 1 ≤ re (f x) for every f ∈ C.

Convex.exists_forall_one_le_re_apply.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {C : Set (WeakDual 𝕜 E)}
  (hC : Convex ℝ C)
  (hCR : ∀ (R : ℝ), IsClosed (C ∩ ⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall 0 R)) {r : ℝ}
  (hr : 0 < r) (hCr : ∀ f ∈ C, r < ‖WeakDual.toStrongDual f‖) : ∃ x, ∀ f ∈ C, 1 ≤ RCLike.re (f x)

Lean

Formalized in Tau Ceti as Convex.exists_forall_one_le_re_apply.

Sources

LeanConvex.exists_forall_one_le_re_apply

Used by 1

Used byKrein–Šmulian theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Banach space theory

TheoremPietsch domination theorem#

Lean

Sources

TheoremPietsch factorization through the closure of the canonical image#

Lean

Sources

TheoremClosed-range theorem#

Lean

Other forms

Sources

TheoremThe Bishop–Phelps theorem#

Lean

Other forms

Sources

TheoremMilman–Pettis theorem#

Lean

Sources

TheoremClarkson's inequality#

Lean

Sources

TheoremJames's basis criterion#

Lean

Sources

AbbreviationTauCeti.AbsolutelySumming#

Lean

Sources

DefinitionTauCeti.HasApproximationProperty#

Lean

Sources

StructureTauCeti.ProjectiveTensor#

Lean

Sources

StructureTauCeti.InjectiveTensor#

Lean

Sources

TheoremThe Bishop–Phelps lemma#

Lean

Sources

TheoremBishop–Phelps support lemma#

Lean

Sources

TheoremGoldstine's theorem#

Lean

Other forms

Sources

TheoremGrothendieck's theorem#

Lean

Other forms

Sources

TheoremHelly's criterion#

Lean

Sources

TheoremHelly's lemma#

Lean

Other forms

Sources

TheoremKrein–Šmulian theorem#

Lean

Sources

TheoremKrein–Šmulian theorem for subspaces#

Lean

Sources

TheoremSeparation lemma of the Krein–Šmulian theorem#

Lean

Sources

TheoremPietsch domination theorem #

TheoremPietsch factorization through the closure of the canonical image #

TheoremClosed-range theorem #

TheoremThe Bishop–Phelps theorem #

TheoremMilman–Pettis theorem #

TheoremClarkson's inequality #

TheoremJames's basis criterion #

AbbreviationTauCeti.AbsolutelySumming #

DefinitionTauCeti.HasApproximationProperty #

StructureTauCeti.ProjectiveTensor #

StructureTauCeti.InjectiveTensor #

TheoremThe Bishop–Phelps lemma #

TheoremBishop–Phelps support lemma #

TheoremGoldstine's theorem #

TheoremGrothendieck's theorem #

TheoremHelly's criterion #

TheoremHelly's lemma #

TheoremKrein–Šmulian theorem #

TheoremKrein–Šmulian theorem for subspaces #

TheoremSeparation lemma of the Krein–Šmulian theorem #