Banach's lemma to Neumann series criterion…

TheoremBanach's lemma#

If every y lies in the closure of the image of the closed ball of radius C * ‖y‖, then every y has a preimage of norm at most 2 * C * ‖y‖. In particular, the map is surjective.

ContinuousLinearMap.exists_preimage_norm_le_of_mem_closure.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1}
  {𝕜' : Type u_2} [Semiring 𝕜] [Semiring 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3}
  [SeminormedAddCommGroup E] [_root_.Module 𝕜 E] [CompleteSpace E] {F : Type u_4}
  [NormedAddCommGroup F] [_root_.Module 𝕜' F] (f : E →SL[σ] F) {C : ℝ}
  (hC : ∀ (y : F), y ∈ closure (⇑f '' Metric.closedBall 0 (C * ‖y‖))) (y : F) :
  ∃ x, f x = y ∧ ‖x‖ ≤ 2 * C * ‖y‖

Lean

Formalized in Tau Ceti as ContinuousLinearMap.exists_preimage_norm_le_of_mem_closure.

Sources

• Tau Ceti documentation: ContinuousLinearMap.exists_preimage_norm_le_of_mem_closure
• Source of ContinuousLinearMap.exists_preimage_norm_le_of_mem_closure in TauCeti/Analysis/Normed/Operator/Banach.lean

LeanContinuousLinearMap.exists_preimage_norm_le_of_mem_closure

Used by 1

Used byClosed-range theorem

TheoremBanach–Steinhaus theorem (Uniform Boundedness Principle) over a Tate ring#

If a family g : ι → E →L[R] F of continuous linear maps from a complete seminormed module E over a Tate ring R is pointwise bounded, then the operator norms ‖g i‖ are uniformly bounded.

TauCeti.NormedRing.IsTate.banach_steinhaus.{u_1, u_2, u_3, u_4} {R : Type u_1} {E : Type u_2}
  {F : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup E]
  [_root_.Module R E] [IsBoundedSMul R E] [SeminormedAddCommGroup F] [_root_.Module R F]
  [IsBoundedSMul R F] [CompleteSpace E] {ι : Type u_4} (g : ι → E →L[R] F)
  (h : ∀ (x : E), ∃ C, ∀ (i : ι), ‖(g i) x‖ ≤ C) : ∃ C, ∀ (i : ι), ‖g i‖ ≤ C

Lean

Formalized in Tau Ceti as TauCeti.NormedRing.IsTate.banach_steinhaus.

Sources

• Tau Ceti documentation: TauCeti.NormedRing.IsTate.banach_steinhaus
• Source of TauCeti.NormedRing.IsTate.banach_steinhaus in TauCeti/Analysis/Normed/Operator/RingOpNorm/UniformBoundedness.lean

LeanTauCeti.NormedRing.IsTate.banach_steinhaus

DefinitionBounded Inverse Theorem#

a bijective continuous linear map from a complete ultrametric seminormed module to a complete normed module over a Tate ring is a continuous linear equivalence.

ContinuousLinearEquiv.ofBijectiveOfIsTate.{u_1, u_2, u_3} {R : Type u_1} {M : Type u_2}
  {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M]
  [IsUltrametricDist M] [CompleteSpace M] [_root_.Module R M] [IsBoundedSMul R M]
  [NormedAddCommGroup N] [CompleteSpace N] [_root_.Module R N] [IsBoundedSMul R N] (f : M →L[R] N)
  (hf : Function.Bijective ⇑f) : M ≃L[R] N

Lean

Formalized in Tau Ceti as ContinuousLinearEquiv.ofBijectiveOfIsTate.

Other forms

Bounded Inverse Theorem for linear equivalences over a Tate ring. Formalized in Tau Ceti as LinearEquiv.continuous_symm_of_isTate.

LinearEquiv.continuous_symm_of_isTate.{u_1, u_2, u_3} {R : Type u_1} {M : Type u_2} {N : Type u_3}
  [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [IsUltrametricDist M]
  [CompleteSpace M] [_root_.Module R M] [IsBoundedSMul R M] [NormedAddCommGroup N] [CompleteSpace N]
  [_root_.Module R N] [IsBoundedSMul R N] (e : M ≃ₗ[R] N) (he : Continuous ⇑e) : Continuous ⇑e.symm

Sources

• Tau Ceti documentation: ContinuousLinearEquiv.ofBijectiveOfIsTate
• Source of ContinuousLinearEquiv.ofBijectiveOfIsTate in TauCeti/Analysis/Normed/Operator/RingOpNorm/OpenMapping.lean

LeanContinuousLinearEquiv.ofBijectiveOfIsTate · LinearEquiv.continuous_symm_of_isTate

Uses 1 · Used by 1

Proof usesOpen Mapping Theorem for normed modules over a Tate ring

Used byClosed Graph Theorem for normed modules over a Tate ring

TheoremClosed Graph Theorem for normed modules over a Tate ring#

a linear map from a complete ultrametric normed module to a complete ultrametric seminormed module whose graph is closed is continuous.

LinearMap.continuous_of_isClosed_graph_of_isTate.{u_1, u_2, u_3} {R : Type u_1} {M : Type u_2}
  {N : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M]
  [IsUltrametricDist M] [CompleteSpace M] [_root_.Module R M] [IsBoundedSMul R M]
  [SeminormedAddCommGroup N] [IsUltrametricDist N] [CompleteSpace N] [_root_.Module R N]
  [IsBoundedSMul R N] (f : M →ₗ[R] N) (hg : IsClosed ↑f.graph) : Continuous ⇑f

Lean

Formalized in Tau Ceti as LinearMap.continuous_of_isClosed_graph_of_isTate.

Sources

• Tau Ceti documentation: LinearMap.continuous_of_isClosed_graph_of_isTate
• Source of LinearMap.continuous_of_isClosed_graph_of_isTate in TauCeti/Analysis/Normed/Operator/RingOpNorm/OpenMapping.lean

LeanLinearMap.continuous_of_isClosed_graph_of_isTate

Uses 1 · Used by 1

Proof usesBounded Inverse Theorem

Used bySequential Closed Graph Theorem for normed modules over a Tate ring

DefinitionThe continuous first isomorphism theorem for Banach algebras#

a continuous surjective algebra homomorphism f : A → B induces an isomorphism of topological algebras A ⧸ ker f ≃ B. Its inverse is continuous by the open mapping theorem; it need not be an isometry.

ContinuousAlgHom.quotientKerEquivOfSurjective.{u_1, u_2, u_3} {𝕜 : Type u_1} {A : Type u_2}
  {B : Type u_3} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A]
  [NormedRing B] [NormedAlgebra 𝕜 B] [CompleteSpace B] (f : A →A[𝕜] B)
  (hf : Function.Surjective ⇑f) : (A ⧸ RingHom.ker f) ≃A[𝕜] B

Lean

Formalized in Tau Ceti as ContinuousAlgHom.quotientKerEquivOfSurjective.

Sources

• Tau Ceti documentation: ContinuousAlgHom.quotientKerEquivOfSurjective
• Source of ContinuousAlgHom.quotientKerEquivOfSurjective in TauCeti/Analysis/Normed/Ring/Quotient.lean

LeanContinuousAlgHom.quotientKerEquivOfSurjective

TheoremCramer's rule bound#

Cramer's rule bound for two linear forms L = a x + b y and L' = a' x + b' y in two variables: the determinant D = a b' - b a' satisfies ‖D‖ max(‖x‖, ‖y‖) ≤ (‖a‖ + ‖b‖ + ‖a'‖ + ‖b'‖) (‖L‖ + ‖L'‖).

TauCeti.norm_det_mul_max_norm_le.{u_1} {𝕜 : Type u_1} [NormedField 𝕜] (a b a' b' x y : 𝕜) :
  ‖a * b' - b * a'‖ * max ‖x‖ ‖y‖ ≤
    (‖a‖ + ‖b‖ + ‖a'‖ + ‖b'‖) * (‖a * x + b * y‖ + ‖a' * x + b' * y‖)

Lean

Formalized in Tau Ceti as TauCeti.norm_det_mul_max_norm_le.

Sources

• Tau Ceti documentation: TauCeti.norm_det_mul_max_norm_le
• Source of TauCeti.norm_det_mul_max_norm_le in TauCeti/Analysis/Normed/Field/LinearForms.lean

LeanTauCeti.norm_det_mul_max_norm_le

Used by 1

Used byThe Thue–Roth inequality for binary forms (Evertse, Theorem 6.3)

TheoremThe Duhamel identity for the exponential of a bounded operator#

For B : X →L[ℝ] X, exp (t B) x - x = ∫₀ᵗ exp (u B) (B x) du.

This is the fundamental theorem of calculus applied to the differentiable orbit u ↦ exp (u B) x, whose derivative is the continuous function u ↦ exp (u B) (B x).

ContinuousLinearMap.exp_smul_apply_sub_eq_intervalIntegral.{u_1} {X : Type u_1}
  [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (B : X →L[ℝ] X) (t : ℝ) (x : X) :
  (NormedSpace.exp (t • B)) x - x = ∫ (u : ℝ) in 0..t, (NormedSpace.exp (u • B)) (B x)

Lean

Formalized in Tau Ceti as ContinuousLinearMap.exp_smul_apply_sub_eq_intervalIntegral.

Sources

• Tau Ceti documentation: ContinuousLinearMap.exp_smul_apply_sub_eq_intervalIntegral
• Source of ContinuousLinearMap.exp_smul_apply_sub_eq_intervalIntegral in TauCeti/Analysis/Normed/Operator/Exponential.lean

LeanContinuousLinearMap.exp_smul_apply_sub_eq_intervalIntegral

Used by 2

Used byHille--Yosida for contraction semigroups · Lumer--Phillips in duality-map form

TheoremEhrling's inequality#

If i : X → Y is a compact operator and j : Y → Z is an injective continuous linear map, then for every ε > 0 there is C ≥ 0 with ‖i x‖ ≤ ε * ‖x‖ + C * ‖j (i x)‖ for all x.

IsCompactOperator.exists_norm_le_mul_norm_add_mul_norm.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1}
  {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [NontriviallyNormedField 𝕜]
  [SeminormedAddCommGroup X] [NormedSpace 𝕜 X] [SeminormedAddCommGroup Y] [NormedSpace 𝕜 Y]
  [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] {i : X →ₗ[𝕜] Y} {j : Y →L[𝕜] Z}
  (hi : IsCompactOperator ⇑i) (hj : Function.Injective ⇑j) {ε : ℝ} (hε : 0 < ε) :
  ∃ C, 0 ≤ C ∧ ∀ (x : X), ‖i x‖ ≤ ε * ‖x‖ + C * ‖j (i x)‖

Lean

Formalized in Tau Ceti as IsCompactOperator.exists_norm_le_mul_norm_add_mul_norm.

Sources

• Tau Ceti documentation: IsCompactOperator.exists_norm_le_mul_norm_add_mul_norm
• Source of IsCompactOperator.exists_norm_le_mul_norm_add_mul_norm in TauCeti/Analysis/Normed/Operator/Compact/Ehrling.lean

LeanIsCompactOperator.exists_norm_le_mul_norm_add_mul_norm

TheoremGantmacher's criterion#

A bounded operator is weakly compact iff its bidual adjoint T** takes values in the canonical image of the codomain in its bidual. No completeness is assumed.

ContinuousLinearMap.isWeaklyCompact_iff_range_subset.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F]
  [NormedSpace 𝕜 F] {T : E →L[𝕜] F} :
  T.IsWeaklyCompact ↔
    Set.range ⇑(ContinuousLinearMap.precomp 𝕜 (ContinuousLinearMap.precomp 𝕜 T)) ⊆
      Set.range ⇑(NormedSpace.inclusionInDoubleDual 𝕜 F)

Lean

Formalized in Tau Ceti as ContinuousLinearMap.isWeaklyCompact_iff_range_subset.

Other forms

Gantmacher's criterion, reverse direction. Formalized in Tau Ceti as ContinuousLinearMap.IsWeaklyCompact.of_range_precomp_precomp_subset.

ContinuousLinearMap.IsWeaklyCompact.of_range_precomp_precomp_subset.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F}
  (h :
    Set.range ⇑(ContinuousLinearMap.precomp 𝕜 (ContinuousLinearMap.precomp 𝕜 T)) ⊆
      Set.range ⇑(NormedSpace.inclusionInDoubleDual 𝕜 F)) :
  T.IsWeaklyCompact

Gantmacher's criterion, forward direction. Formalized in Tau Ceti as ContinuousLinearMap.IsWeaklyCompact.range_precomp_precomp_subset.

ContinuousLinearMap.IsWeaklyCompact.range_precomp_precomp_subset.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (hT : T.IsWeaklyCompact) :
  Set.range ⇑(ContinuousLinearMap.precomp 𝕜 (ContinuousLinearMap.precomp 𝕜 T)) ⊆
    Set.range ⇑(NormedSpace.inclusionInDoubleDual 𝕜 F)

Sources

• Tau Ceti documentation: ContinuousLinearMap.isWeaklyCompact_iff_range_subset
• Source of ContinuousLinearMap.isWeaklyCompact_iff_range_subset in TauCeti/Analysis/Normed/Operator/WeaklyCompact/Basic.lean

LeanContinuousLinearMap.isWeaklyCompact_iff_range_subset · ContinuousLinearMap.IsWeaklyCompact.of_range_precomp_precomp_subset · ContinuousLinearMap.IsWeaklyCompact.range_precomp_precomp_subset

Uses 1 · Used by 1

Proof usesGoldstine's theorem

Used byGantmacher's theorem

TheoremGantmacher's theorem#

An operator into a Banach space is weakly compact iff its adjoint is weakly compact.

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

Lean

Formalized in Tau Ceti as ContinuousLinearMap.isWeaklyCompact_precomp_iff.

Other forms

Gantmacher's theorem, reverse direction. Formalized in Tau Ceti as ContinuousLinearMap.IsWeaklyCompact.of_precomp.

ContinuousLinearMap.IsWeaklyCompact.of_precomp.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F]
  [NormedSpace 𝕜 F] [CompleteSpace F] {T : E →L[𝕜] F}
  (hT : (ContinuousLinearMap.precomp 𝕜 T).IsWeaklyCompact) : T.IsWeaklyCompact

Gantmacher's theorem, forward direction. Formalized in Tau Ceti as ContinuousLinearMap.IsWeaklyCompact.precomp.

ContinuousLinearMap.IsWeaklyCompact.precomp.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F]
  [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (hT : T.IsWeaklyCompact) :
  (ContinuousLinearMap.precomp 𝕜 T).IsWeaklyCompact

Sources

• Tau Ceti documentation: ContinuousLinearMap.isWeaklyCompact_precomp_iff
• Source of ContinuousLinearMap.isWeaklyCompact_precomp_iff in TauCeti/Analysis/Normed/Operator/WeaklyCompact/Basic.lean

LeanContinuousLinearMap.isWeaklyCompact_precomp_iff · ContinuousLinearMap.IsWeaklyCompact.of_precomp · ContinuousLinearMap.IsWeaklyCompact.precomp

Uses 1

Proof usesGantmacher's criterion

TheoremGelfand's formula in a nonunital complex Banach algebra#

the spectral radius of a, computed from its quasispectrum, is the Gelfand radius of its image in the ℓ¹ unitization.

TauCeti.spectralRadius_eq_gelfandRadius_toLp_inr.{u_1} {A : Type u_1} [NonUnitalNormedRing A]
  [NormedSpace ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [CompleteSpace A] (a : A) :
  spectralRadius ℂ a = ENNReal.ofReal (gelfandRadius (WithLp.toLp 1 ↑a))

Lean

Formalized in Tau Ceti as TauCeti.spectralRadius_eq_gelfandRadius_toLp_inr.

Sources

• Tau Ceti documentation: TauCeti.spectralRadius_eq_gelfandRadius_toLp_inr
• Source of TauCeti.spectralRadius_eq_gelfandRadius_toLp_inr in TauCeti/Analysis/Normed/Algebra/GelfandRadius.lean

LeanTauCeti.spectralRadius_eq_gelfandRadius_toLp_inr

Used by 1

Used byJohnson's theorem

TheoremGrothendieck's lemma#

In a real or complex Banach space, a set has weakly compact closure if, for every ε > 0, each of its points lies within norm distance ε of a fixed weakly compact set.

TauCeti.isCompact_closure_toWeakSpace_of_forall_exists_isCompact.{u_1, u_2} {𝕜 : Type u_1}
  {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {A : Set E}
  (h : ∀ ε > 0, ∃ K, IsCompact (⇑(toWeakSpace 𝕜 E) '' K) ∧ ∀ x ∈ A, ∃ y ∈ K, ‖x - y‖ ≤ ε) :
  IsCompact (closure (⇑(toWeakSpace 𝕜 E) '' A))

Lean

Formalized in Tau Ceti as TauCeti.isCompact_closure_toWeakSpace_of_forall_exists_isCompact.

Sources

• Tau Ceti documentation: TauCeti.isCompact_closure_toWeakSpace_of_forall_exists_isCompact
• Source of TauCeti.isCompact_closure_toWeakSpace_of_forall_exists_isCompact in TauCeti/Analysis/Normed/Module/WeakSpace/Approximation.lean

LeanTauCeti.isCompact_closure_toWeakSpace_of_forall_exists_isCompact

Used by 1

Used byDunford–Pettis theorem

TheoremHölder's inequality for weak norms#

Multiplying a finite family by scalar weights c multiplies its weak norm by at most the ℓˢ norm of the weights, when 1 / p = 1 / s + 1 / q with finite p and q.

TauCeti.weakLpNorm_smul_le.{u_1, u_2, u_4} {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_4}
  [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Fintype ι] (p : ENNReal)
  [Fact (1 ≤ p)] {q : ENNReal} [Fact (1 ≤ q)] {s : ℝ} (hspq : s.HolderTriple q.toReal p.toReal)
  (c : ι → 𝕜) (x : ι → E) :
  ((TauCeti.weakLpNorm p) fun i => c i • x i) ≤
    (∑ i, ‖c i‖ ^ s) ^ (1 / s) * (TauCeti.weakLpNorm q) x

Lean

Formalized in Tau Ceti as TauCeti.weakLpNorm_smul_le.

Sources

• Tau Ceti documentation: TauCeti.weakLpNorm_smul_le
• Source of TauCeti.weakLpNorm_smul_le in TauCeti/Analysis/Normed/Lp/Weak.lean

LeanTauCeti.weakLpNorm_smul_le

TheoremJohnson's theorem#

A surjective homomorphism θ : A → B of complex Banach algebras, not assumed continuous, is continuous when B is unital with zero Jacobson radical.

NonUnitalAlgHom.continuous_of_surjective_of_jacobson_eq_bot.{u_1, u_2} {A : Type u_1} {B : Type u_2}
  [NonUnitalNormedRing A] [NormedSpace ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A]
  [CompleteSpace A] [NormedRing B] [NormedAlgebra ℂ B] [CompleteSpace B] (θ : A →ₙₐ[ℂ] B)
  (hθ : Function.Surjective ⇑θ) (hB : Ring.jacobson B = ⊥) : Continuous ⇑θ

Lean

Formalized in Tau Ceti as NonUnitalAlgHom.continuous_of_surjective_of_jacobson_eq_bot.

Other forms

Johnson's theorem, nonunital form. Formalized in Tau Ceti as NonUnitalAlgHom.continuous_of_surjective_of_nonUnitalJacobson_eq_bot.

NonUnitalAlgHom.continuous_of_surjective_of_nonUnitalJacobson_eq_bot.{u_1, u_3} {A : Type u_1}
  [NonUnitalNormedRing A] [NormedSpace ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A]
  [CompleteSpace A] {B : Type u_3} [NonUnitalNormedRing B] [NormedSpace ℂ B] [IsScalarTower ℂ B B]
  [SMulCommClass ℂ B B] [CompleteSpace B] (θ : A →ₙₐ[ℂ] B) (hθ : Function.Surjective ⇑θ)
  (hB : TauCeti.nonUnitalJacobson ℂ B = ⊥) : Continuous ⇑θ

Sources

• Tau Ceti documentation: NonUnitalAlgHom.continuous_of_surjective_of_jacobson_eq_bot
• Source of NonUnitalAlgHom.continuous_of_surjective_of_jacobson_eq_bot in TauCeti/Analysis/Normed/Algebra/SeparatingIdeal/Semisimple.lean

LeanNonUnitalAlgHom.continuous_of_surjective_of_jacobson_eq_bot · NonUnitalAlgHom.continuous_of_surjective_of_nonUnitalJacobson_eq_bot

Uses 6 · Used by 1

Statement usesTauCeti.nonUnitalJacobson

Proof usesGelfand's formula in a nonunital complex Banach algebra · LinearMap.continuous_iff_separatingSpace_eq_bot · LinearMap.separatingSpace · Rickart's scalar-commutant theorem · Sinclair's stability lemma

Used byJohnson's uniqueness-of-norm theorem

TheoremJohnson's uniqueness-of-norm theorem#

On a unital complex algebra A with zero Jacobson radical, any two algebra norms under which A is complete are equivalent.

AlgebraNorm.exists_le_mul_and_le_mul_of_jacobson_eq_bot.{u_1} {A : Type u_1} [Ring A] [Algebra ℂ A]
  (f g : AlgebraNorm ℂ A) (hf : CompleteSpace A) (hg : CompleteSpace A) (hA : Ring.jacobson A = ⊥) :
  ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : A), f x ≤ C₁ * g x ∧ g x ≤ C₂ * f x

Lean

Formalized in Tau Ceti as AlgebraNorm.exists_le_mul_and_le_mul_of_jacobson_eq_bot.

Other forms

Johnson's uniqueness-of-norm theorem. Formalized in Tau Ceti as RingNorm.exists_le_mul_and_le_mul_of_nonUnitalJacobson_eq_bot.

RingNorm.exists_le_mul_and_le_mul_of_nonUnitalJacobson_eq_bot.{u_1} {A : Type u_1} [NonUnitalRing A]
  [_root_.Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] (f g : RingNorm A)
  (hfs : ∀ (c : ℂ) (x : A), f (c • x) ≤ ‖c‖ * f x) (hgs : ∀ (c : ℂ) (x : A), g (c • x) ≤ ‖c‖ * g x)
  (hf : CompleteSpace A) (hg : CompleteSpace A) (hA : TauCeti.nonUnitalJacobson ℂ A = ⊥) :
  ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : A), f x ≤ C₁ * g x ∧ g x ≤ C₂ * f x

Sources

• Tau Ceti documentation: AlgebraNorm.exists_le_mul_and_le_mul_of_jacobson_eq_bot
• Source of AlgebraNorm.exists_le_mul_and_le_mul_of_jacobson_eq_bot in TauCeti/Analysis/Normed/Algebra/SeparatingIdeal/NormUniqueness.lean

LeanAlgebraNorm.exists_le_mul_and_le_mul_of_jacobson_eq_bot · RingNorm.exists_le_mul_and_le_mul_of_nonUnitalJacobson_eq_bot

Uses 2

Statement usesTauCeti.nonUnitalJacobson

Proof usesJohnson's theorem

TheoremJohnson–Sinclair theorem, nonunital form#

Let B be a complex Banach algebra, not necessarily unital, with zero Jacobson radical. Every linear map D : B → B satisfying the Leibniz rule D (x * y) = x * D y + D x * y is continuous.

LinearMap.continuous_of_derivation_of_nonUnitalJacobson_eq_bot.{u_1} {B : Type u_1}
  [NonUnitalNormedRing B] [NormedSpace ℂ B] [IsScalarTower ℂ B B] [SMulCommClass ℂ B B]
  [CompleteSpace B] (D : B →ₗ[ℂ] B) (hD : ∀ (x y : B), D (x * y) = x * D y + D x * y)
  (hB : TauCeti.nonUnitalJacobson ℂ B = ⊥) : Continuous ⇑D

Lean

Formalized in Tau Ceti as LinearMap.continuous_of_derivation_of_nonUnitalJacobson_eq_bot.

Other forms

Johnson–Sinclair theorem: derivations of semisimple Banach algebras are continuous. Formalized in Tau Ceti as LinearMap.continuous_of_derivation_of_jacobson_eq_bot.

LinearMap.continuous_of_derivation_of_jacobson_eq_bot.{u_1} {B : Type u_1} [NormedRing B]
  [NormedAlgebra ℂ B] [CompleteSpace B] (D : B →ₗ[ℂ] B)
  (hD : ∀ (x y : B), D (x * y) = x * D y + D x * y) (hB : Ring.jacobson B = ⊥) : Continuous ⇑D

Sources

• Tau Ceti documentation: LinearMap.continuous_of_derivation_of_nonUnitalJacobson_eq_bot
• Source of LinearMap.continuous_of_derivation_of_nonUnitalJacobson_eq_bot in TauCeti/Analysis/Normed/Algebra/SeparatingIdeal/Derivation.lean

LeanLinearMap.continuous_of_derivation_of_nonUnitalJacobson_eq_bot · LinearMap.continuous_of_derivation_of_jacobson_eq_bot

Uses 5

Statement usesTauCeti.nonUnitalJacobson

Proof usesLinearMap.continuous_iff_separatingSpace_eq_bot · LinearMap.separatingSpace · Rickart's scalar-commutant theorem · Sinclair's stability lemma

TheoremLocal Neumann formula for the resolvent#

Inside the ball ‖mu - lambda‖ * ‖R(lambda)‖ < 1, the resolvent at mu is obtained by multiplying R(lambda) by the ring inverse of 1 - (lambda - mu) R(lambda).

TauCeti.LinearPMap.resolvent_eq_mul_inverse_one_sub.{u_1, u_2} {𝕜 : Type u_1} {X : Type u_2}
  [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X]
  [HasSummableGeomSeries (X →L[𝕜] X)] {A : X →ₗ.[𝕜] X} {lambda mu : 𝕜} (h : lambda ∈ A.resolventSet)
  (hmu : ‖mu - lambda‖ * ‖A.resolvent lambda‖ < 1) :
  A.resolvent mu = A.resolvent lambda * Ring.inverse (1 - (lambda - mu) • A.resolvent lambda)

Lean

Formalized in Tau Ceti as TauCeti.LinearPMap.resolvent_eq_mul_inverse_one_sub.

Sources

• Tau Ceti documentation: TauCeti.LinearPMap.resolvent_eq_mul_inverse_one_sub
• Source of TauCeti.LinearPMap.resolvent_eq_mul_inverse_one_sub in TauCeti/Analysis/Normed/Operator/Resolvent/Unbounded.lean

LeanTauCeti.LinearPMap.resolvent_eq_mul_inverse_one_sub

TheoremMazur's lemma, in sequential form#

choose a finite real convex combination from the nth tail for every n, so that the combinations converge in norm to the weak limit.

TauCeti.exists_tendsto_sum_smul_of_tendsto_weak.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E] {u : ℕ → E}
  {x : E}
  (hu :
    Filter.Tendsto (fun n => (toWeakSpace 𝕜 E) (u n)) Filter.atTop (nhds ((toWeakSpace 𝕜 E) x))) :
  ∃ s w,
    (∀ (n i : ℕ), i ∈ s n → 0 ≤ w n i) ∧
      (∀ (n : ℕ), ∑ i ∈ s n, w n i = 1) ∧
        Filter.Tendsto (fun n => ∑ i ∈ s n, w n i • u (n + i)) Filter.atTop (nhds x)

Lean

Formalized in Tau Ceti as TauCeti.exists_tendsto_sum_smul_of_tendsto_weak.

Other forms

Mazur's lemma, with explicit finite coefficients. Formalized in Tau Ceti as TauCeti.exists_sum_smul_norm_sub_lt_of_tendsto_weak.

TauCeti.exists_sum_smul_norm_sub_lt_of_tendsto_weak.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2}
  [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E]
  {u : ℕ → E} {x : E}
  (hu : Filter.Tendsto (fun n => (toWeakSpace 𝕜 E) (u n)) Filter.atTop (nhds ((toWeakSpace 𝕜 E) x)))
  (n : ℕ) {ε : ℝ} (hε : 0 < ε) :
  ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ ∑ i ∈ s, w i = 1 ∧ ‖∑ i ∈ s, w i • u (n + i) - x‖ < ε

Sources

• Tau Ceti documentation: TauCeti.exists_tendsto_sum_smul_of_tendsto_weak
• Source of TauCeti.exists_tendsto_sum_smul_of_tendsto_weak in TauCeti/Analysis/Normed/Module/Mazur.lean

LeanTauCeti.exists_tendsto_sum_smul_of_tendsto_weak · TauCeti.exists_sum_smul_norm_sub_lt_of_tendsto_weak

TheoremThe method of continuity (Gilbarg–Trudinger, Theorem 5.2)#

Let E be a Banach space and L₀, L₁ : E →L[𝕜] F. If the operators L t = (1 - t) L₀ + t L₁ satisfy the a priori estimate ‖x‖ ≤ C * ‖L t x‖ for every t ∈ [0, 1], then L₀ is surjective if and only if L₁ is.

ContinuousLinearMap.surjective_iff_of_forall_norm_le_lineMap.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {C : ℝ} [NormedSpace ℝ F]
  [SMulCommClass 𝕜 ℝ F] {L₀ L₁ : E →L[𝕜] F}
  (hC : ∀ t ∈ Set.Icc 0 1, ∀ (x : E), ‖x‖ ≤ C * ‖((AffineMap.lineMap L₀ L₁) t) x‖) :
  Function.Surjective ⇑L₀ ↔ Function.Surjective ⇑L₁

Lean

Formalized in Tau Ceti as ContinuousLinearMap.surjective_iff_of_forall_norm_le_lineMap.

Sources

• Tau Ceti documentation: ContinuousLinearMap.surjective_iff_of_forall_norm_le_lineMap
• Source of ContinuousLinearMap.surjective_iff_of_forall_norm_le_lineMap in TauCeti/Analysis/Normed/Operator/MethodOfContinuity.lean

LeanContinuousLinearMap.surjective_iff_of_forall_norm_le_lineMap

TheoremNeumann series criterion (TauCeti.IsNormMulUnit.of_norm_sub_lt)#

In an ultrametric norm-one ring with summable geometric series, an element whose distance from a multiplicative unit u is less than ‖u‖ is a multiplicative unit.

TauCeti.IsNormMulUnit.of_norm_sub_lt.{u_1} {A : Type u_1} [NormedRing A] [NormOneClass A]
  [HasSummableGeomSeries A] [IsUltrametricDist A] {u f : A} (hu : TauCeti.IsNormMulUnit u)
  (hf : ‖f - u‖ < ‖u‖) : TauCeti.IsNormMulUnit f

Lean

Formalized in Tau Ceti as TauCeti.IsNormMulUnit.of_norm_sub_lt.

Sources

• Tau Ceti documentation: TauCeti.IsNormMulUnit.of_norm_sub_lt
• Source of TauCeti.IsNormMulUnit.of_norm_sub_lt in TauCeti/Analysis/Normed/Ring/MulUnit.lean

LeanTauCeti.IsNormMulUnit.of_norm_sub_lt

Used by 1

Used byNeumann series criterion (MvPowerSeries.isNormMulUnit_of_norm_sub_C_lt)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.