Other results
Results named in the rest of Tau Ceti's TauCeti.Analysis modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremThe bicommutant theorem#
a unital star subalgebra equals its double commutant if and only if it is weak operator closed.
StarSubalgebra.double_commutant_iff_isClosed_image_ofCLM.{u_1, u_2} {𝕜 : Type u_1} {H : Type u_2}
[RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H]
(S : StarSubalgebra 𝕜 (H →L[𝕜] H)) :
(↑S).centralizer.centralizer = ↑S ↔ IsClosed (ContinuousLinearMapWOT.ofCLM '' ↑S)
Lean
Formalized in Tau Ceti as StarSubalgebra.double_commutant_iff_isClosed_image_ofCLM.
Sources
Uses 1
TheoremThe bipolar theorem#
the bipolar of a nonempty absolutely convex set equals its closure in the original locally convex topology.
AbsConvex.bipolar_eq_closure.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E]
[_root_.Module 𝕜 E] [TopologicalSpace E] [_root_.Module ℝ E] [IsScalarTower ℝ 𝕜 E]
[IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] {s : Set E}
(hs : AbsConvex 𝕜 s) (hne : s.Nonempty) :
(topDualPairing 𝕜 E).polar (StrongDual.polar 𝕜 s) = closure s
Used by 1
TheoremThe bipolar theorem for an arbitrary set#
Its bipolar is the closed absolutely convex hull of the set together with zero, including when the set is empty.
StrongDual.bipolar_eq_closedAbsConvexHull.{u_1, u_2} (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜]
[AddCommGroup E] [_root_.Module 𝕜 E] [TopologicalSpace E] [_root_.Module ℝ E]
[IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E]
(s : Set E) :
(topDualPairing 𝕜 E).polar (StrongDual.polar 𝕜 s) = (closedAbsConvexHull 𝕜) (insert 0 s)
Uses 1
TheoremDiscrete Grönwall bound under coercivity#
Let D n ≥ 0 with D 0 = 0 grow by steps
D (n + 1) ≤ D n + d n whose squared lengths are paid for by an energy e,
d n ² ≤ 2τ (e n - e (n + 1)), and let the energy satisfy the coercivity bound
2τ' (A - e n) ≤ D n ², where 4τ ≤ τ'. Then D n ² ≤ 2τ' (e 0 - A) (1 + 8τ / τ')ⁿ.
With c = τ + τ' / 4, the quantity N n = D n ² + 2c (e n - A) dominates D n ² / 2 by the
coercivity bound, and grows at most by the factor 1 + 8τ / τ' per step by the triangle
inequality, Young's inequality and the energy decrease along a step.
TauCeti.sq_le_mul_one_add_div_pow_of_sq_le_mul_sub {D d e : ℕ → ℝ} {τ τ' A : ℝ} (hτ : 0 < τ)
(hττ' : 4 * τ ≤ τ') (hD0 : D 0 = 0) (hD : ∀ (n : ℕ), 0 ≤ D n)
(htri : ∀ (n : ℕ), D (n + 1) ≤ D n + d n) (hstep : ∀ (n : ℕ), d n ^ 2 ≤ 2 * τ * (e n - e (n + 1)))
(hcoer : ∀ (n : ℕ), 2 * τ' * (A - e n) ≤ D n ^ 2) (n : ℕ) :
D n ^ 2 ≤ 2 * τ' * (e 0 - A) * (1 + 8 * τ / τ') ^ n
Lean
Formalized in Tau Ceti as TauCeti.sq_le_mul_one_add_div_pow_of_sq_le_mul_sub.
Sources
Used by 1
TheoremEvertse's lemma#
Evertse's lemma (Evertse; Bombieri–Gubler, Lemma 7.5.29), for a field K with a set T
of absolute values at which a subset R approximates every family of targets simultaneously,
v (ξ + γ v) ≤ A v. Let x 0, …, x (m - 1) be linearly independent in V, and at each v ∈ T
let the forms L v k separate the points of V, with weights ν v k > 0 and a nondecreasing
μ v bounding v (L v k (x j)) ≤ ν v k * μ v j. Then there are coefficients ξ j l ∈ R and
permutations π v such that y j = x j + ∑ l < j, ξ j l • x l satisfies
v (L v (π v i) (y j)) ≤ 2 ^ (2 m + 1) * max 1 (A v) * (ν v (π v i) * min (μ v i) (μ v j))
at every v ∈ T, and the same bound without the constant at every nonarchimedean v ∈ T with
A v ≤ 1.
AbsoluteValue.exists_evertse_of_approx.{u_1, u_2} {K : Type u_1} {V : Type u_2} [Field K]
[AddCommGroup V] [_root_.Module K V] {m : ℕ} {T : Set (AbsoluteValue K ℝ)} {R : Set K}
{A : AbsoluteValue K ℝ → ℝ}
(happrox : ∀ (γ : AbsoluteValue K ℝ → K), ∃ ξ ∈ R, ∀ v ∈ T, v (ξ + γ v) ≤ A v)
{L : AbsoluteValue K ℝ → Fin m → Module.Dual K V}
(hL : ∀ v ∈ T, ∀ (z : V), (∀ (k : Fin m), (L v k) z = 0) → z = 0) {x : Fin m → V}
(hx : LinearIndependent K x) {ν μ : AbsoluteValue K ℝ → Fin m → ℝ}
(hν : ∀ v ∈ T, ∀ (k : Fin m), 0 < ν v k) (hμ : ∀ v ∈ T, Monotone (μ v))
(hLx : ∀ v ∈ T, ∀ (k j : Fin m), v ((L v k) (x j)) ≤ ν v k * μ v j) :
∃ ξ π,
(∀ (j l : Fin m), ξ j l ∈ R) ∧
(∀ v ∈ T,
∀ (i j : Fin m),
v ((L v ((π v) i)) (x j + ∑ l with l < j, ξ j l • x l)) ≤
2 ^ (2 * m + 1) * max 1 (A v) * (ν v ((π v) i) * min (μ v i) (μ v j))) ∧
∀ v ∈ T,
IsNonarchimedean ⇑v →
A v ≤ 1 →
∀ (i j : Fin m),
v ((L v ((π v) i)) (x j + ∑ l with l < j, ξ j l • x l)) ≤
ν v ((π v) i) * min (μ v i) (μ v j)
Used by 1
TheoremFirst-order Taylor bound for a Hölder derivative#
If g has derivative g' within s
and g' is α-Hölder with constant H on s, then for a segment from x to x + w contained
in s, the error of the linear approximation is at most H ‖w‖^(1 + α).
HolderOnWith.norm_image_sub_sub_le_of_hasFDerivWithinAt.{u_1, u_2} {E : Type u_1} {F : Type u_2}
[NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set E}
{g : E → F} {g' : E → E →L[ℝ] F} {H α : NNReal} (hH : HolderOnWith H α g' s)
(hg : ∀ y ∈ s, HasFDerivWithinAt g (g' y) s y) {x w : E} (hxw : segment ℝ x (x + w) ⊆ s) :
‖g (x + w) - g x - (g' x) w‖ ≤ ↑H * ‖w‖ ^ (1 + ↑α)
Lean
Formalized in Tau Ceti as HolderOnWith.norm_image_sub_sub_le_of_hasFDerivWithinAt.
Sources
Used by 1
TheoremFlux-divergence form of Green's theorem for a simple closed absolutely continuous curve#
the boundary integral of X dy - Y dx equals Contour.jordanSign γ a b ∈ {1, -1} times the
divergence integral over filledHull (γ '' uIcc a b) \ (γ '' uIcc a b).
TauCeti.Green.green_ac_flux_jordan {γ : ℝ → ℂ} {a b : ℝ} {U : Set ℂ} {X Y : ℂ → ℝ} (hab : a < b)
(hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b)
(hinj : Set.InjOn γ (Set.Ico a b)) (hU : IsOpen U)
(hregion : TauCeti.filledHull (γ '' Set.uIcc a b) ⊆ U) (hX : ContDiffOn ℝ 1 X U)
(hY : ContDiffOn ℝ 1 Y U) :
IntervalIntegrable (fun t => X (γ t) * (deriv γ t).im - Y (γ t) * (deriv γ t).re)
MeasureTheory.volume a b ∧
MeasureTheory.IntegrableOn (fun z => (fderiv ℝ X z) 1 + (fderiv ℝ Y z) Complex.I)
(TauCeti.filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b) MeasureTheory.volume ∧
∫ (t : ℝ) in a..b, X (γ t) * (deriv γ t).im - Y (γ t) * (deriv γ t).re =
↑(TauCeti.Contour.jordanSign γ a b) *
∫ (z : ℂ) in TauCeti.filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b,
(fderiv ℝ X z) 1 + (fderiv ℝ Y z) Complex.I
Uses 2
TheoremThe Gagliardo–Nirenberg–Sobolev inequality for integrable functions#
Let E have
dimension n ≥ 2 and let p = n / (n - 1). Every integrable C¹ function u satisfies
‖u‖_p ≤ C ‖Du‖₁, with ‖Du‖₁ finite or infinite, where C is the constant
MeasureTheory.eLpNormLESNormFDerivOneConst μ p of the compactly supported case
MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one.
TauCeti.eLpNorm_le_eLpNorm_fderiv_one_of_integrable.{u_1, u_2} {E : Type u_1} [NormedAddCommGroup E]
[NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E]
(μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {F : Type u_2} [NormedAddCommGroup F]
[NormedSpace ℝ F] {u : E → F} (hu : ContDiff ℝ 1 u) (hi : MeasureTheory.Integrable u μ)
{p : NNReal} (hp : (↑(Module.finrank ℝ E)).HolderConjugate p) :
MeasureTheory.eLpNorm u (↑p) μ ≤
↑(MeasureTheory.eLpNormLESNormFDerivOneConst μ ↑p) * MeasureTheory.eLpNorm (fderiv ℝ u) 1 μ
Lean
Formalized in Tau Ceti as TauCeti.eLpNorm_le_eLpNorm_fderiv_one_of_integrable.
Sources
Used by 1
TheoremGreen's theorem for a simple closed absolutely continuous curve#
with no supplied index
hypothesis, both the boundary circulation and the interior curl are integrable and the circulation
equals Contour.jordanSign γ a b ∈ {1, -1} times the integral of curl P Q over the bounded inside
filledHull (γ '' uIcc a b) \ (γ '' uIcc a b).
TauCeti.Green.green_ac_jordan {γ : ℝ → ℂ} {a b : ℝ} {U : Set ℂ} {P Q : ℂ → ℝ} (hab : a < b)
(hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b)
(hinj : Set.InjOn γ (Set.Ico a b)) (hU : IsOpen U)
(hregion : TauCeti.filledHull (γ '' Set.uIcc a b) ⊆ U) (hP : ContDiffOn ℝ 1 P U)
(hQ : ContDiffOn ℝ 1 Q U) :
IntervalIntegrable (TauCeti.Green.circulationFun P Q γ) MeasureTheory.volume a b ∧
MeasureTheory.IntegrableOn (TauCeti.Green.curl P Q)
(TauCeti.filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b) MeasureTheory.volume ∧
∫ (t : ℝ) in a..b, TauCeti.Green.circulationFun P Q γ t =
↑(TauCeti.Contour.jordanSign γ a b) *
∫ (z : ℂ) in TauCeti.filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b,
TauCeti.Green.curl P Q z
Uses 3 · Used by 1
TheoremHölder's inequality for unconditional sums in ℝ≥0∞#
for conjugate exponents p and q,
∑' i, f i * g i ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q).
No summability hypotheses are needed; both sides may be infinite.
ENNReal.inner_le_Lp_mul_Lq_tsum.{u_1} {ι : Type u_1} (f g : ι → ENNReal) {p q : ℝ}
(hpq : p.HolderConjugate q) :
∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
TheoremJensen's inequality for convolution#
If Φ is convex and monotone on [0, ∞) and ρ
is a probability kernel, then at every point Φ(‖(ρ ⋆ g)(x)‖) ≤ ∫ ρ(t) Φ(‖g(x - t)‖) dt, in
extended nonnegative form.
ConvexOn.ofReal_map_norm_convolution_le_lintegral.{u_1, u_2} {G : Type u_1} {F : Type u_2}
[MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G]
{μ : MeasureTheory.Measure G} [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant]
[NormedAddCommGroup F] [NormedSpace ℝ F] {Φ : ℝ → ℝ} {ρ : G → ℝ} (hΦ : ConvexOn ℝ (Set.Ici 0) Φ)
(hΦm : MonotoneOn Φ (Set.Ici 0)) (hρ0 : 0 ≤ᵐ[μ] ρ) (hρ1 : ∫ (t : G), ρ t ∂μ = 1) {g : G → F}
(hg : MeasureTheory.AEStronglyMeasurable g μ) (x : G) :
ENNReal.ofReal (Φ ‖MeasureTheory.convolution ρ g (ContinuousLinearMap.lsmul ℝ ℝ) μ x‖) ≤
∫⁻ (t : G), ENNReal.ofReal (ρ t) * ENNReal.ofReal (Φ ‖g (x - t)‖) ∂μ
Lean
Formalized in Tau Ceti as ConvexOn.ofReal_map_norm_convolution_le_lintegral.
Sources
Used by 1
TheoremMinkowski's inequality for unconditional sums in ℝ≥0∞#
for 1 ≤ p,
(∑' i, (f i + g i) ^ p) ^ (1 / p) ≤ (∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p).
No summability hypotheses are needed; both sides may be infinite.
ENNReal.Lp_add_le_tsum.{u_1} {ι : Type u_1} (f g : ι → ENNReal) {p : ℝ} (hp : 1 ≤ p) :
(∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤
(∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
Used by 1
TheoremStampacchia's lemma#
Let φ be nonnegative and antitone on [k₀, ∞), with
φ h ≤ (M / (h - k)) ^ α * φ k ^ β whenever k₀ ≤ k < h,
for constants M > 0, α > 0 and β > 1. Then φ (k₀ + d) = 0, where
d = M * φ k₀ ^ ((β - 1) / α) * 2 ^ (β / (β - 1)).
TauCeti.apply_add_eq_zero_of_le_div_sub_rpow_mul_rpow {φ : ℝ → ℝ} {k₀ M α β : ℝ} (hM : 0 < M)
(hα : 0 < α) (hβ : 1 < β) (hφ : ∀ (h : ℝ), k₀ ≤ h → 0 ≤ φ h) (hanti : AntitoneOn φ (Set.Ici k₀))
(hrec : ∀ (k h : ℝ), k₀ ≤ k → k < h → φ h ≤ (M / (h - k)) ^ α * φ k ^ β) :
φ (k₀ + M * φ k₀ ^ ((β - 1) / α) * 2 ^ (β / (β - 1))) = 0
Lean
Formalized in Tau Ceti as TauCeti.apply_add_eq_zero_of_le_div_sub_rpow_mul_rpow.
Sources
Used by 1
TheoremThe von Neumann density theorem#
An operator x in the double commutant of a unital star
subalgebra S of the bounded operators on a Hilbert space is a strong-operator limit of elements
of S: for every finite family of vectors v i and every ε > 0 there is s ∈ S with
‖x (v i) - s (v i)‖ < ε for all i.
StarSubalgebra.exists_forall_norm_sub_apply_lt_of_mem_centralizer_centralizer.{u_1, u_2, u_3}
{𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H]
[CompleteSpace H] (S : StarSubalgebra 𝕜 (H →L[𝕜] H)) {x : H →L[𝕜] H}
(hx : x ∈ (↑S).centralizer.centralizer) {ι : Type u_3} [Finite ι] (v : ι → H) {ε : ℝ}
(hε : 0 < ε) : ∃ s ∈ S, ∀ (i : ι), ‖x (v i) - s (v i)‖ < ε
Lean
Formalized in Tau Ceti as StarSubalgebra.exists_forall_norm_sub_apply_lt_of_mem_centralizer_centralizer.
Other forms
The von Neumann density theorem for a generated von Neumann algebra. Formalized in Tau Ceti as VonNeumannAlgebra.exists_forall_norm_sub_apply_lt_of_mem_adjoin.
VonNeumannAlgebra.exists_forall_norm_sub_apply_lt_of_mem_adjoin.{u_1, u_2} {H : Type u_1}
[NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s : Set (H →L[ℂ] H)}
{x : H →L[ℂ] H} (hx : x ∈ VonNeumannAlgebra.adjoin s) {ι : Type u_2} [Finite ι] (v : ι → H)
{ε : ℝ} (hε : 0 < ε) : ∃ t ∈ StarAlgebra.adjoin ℂ s, ∀ (i : ι), ‖x (v i) - t (v i)‖ < ε
The von Neumann density theorem for one vector. Formalized in Tau Ceti as StarSubalgebra.apply_mem_closure_of_mem_centralizer_centralizer.
StarSubalgebra.apply_mem_closure_of_mem_centralizer_centralizer.{u_1, u_2} {𝕜 : Type u_1}
{H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H]
(S : StarSubalgebra 𝕜 (H →L[𝕜] H)) {x : H →L[𝕜] H} (hx : x ∈ (↑S).centralizer.centralizer)
(v : H) : x v ∈ closure ((fun s => s v) '' ↑S)
Sources
Used by 1
TheoremYoung's inequality L¹ ⋆ L² ⊆ L²#
For extended nonnegative functions on a group with a
left-invariant measure, ∫⁻ (f ⋆ₗ[μ] g) ^ 2 ≤ (∫⁻ f) ^ 2 * ∫⁻ g ^ 2.
MeasureTheory.lintegral_lconvolution_sq_le.{u_1} {G : Type u_1} {mG : MeasurableSpace G}
[AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] {μ : MeasureTheory.Measure G}
[MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] {f g : G → ENNReal} (hf : AEMeasurable f μ)
(hg : AEMeasurable g μ) :
∫⁻ (x : G), MeasureTheory.lconvolution f g μ x ^ 2 ∂μ ≤
(∫⁻ (y : G), f y ∂μ) ^ 2 * ∫⁻ (x : G), g x ^ 2 ∂μ
TheoremThe zero-spatial BCR theorem is the Hausdorff--Bernstein--Widder theorem#
For a real function f, the bounded, continuous positive-definite condition on
(t, _) ↦ f t : ℝ≥0 × PUnit → ℂ holds exactly when f is continuous on [0, ∞) and completely
monotone on (0, ∞).
TauCeti.bcr_zero_spatial_iff_hausdorff_bernstein_widder (f : ℝ → ℝ) :
(TauCeti.IsSemigroupGroupPD fun x => ↑(f ↑x.1)) ∧
(Continuous fun x => ↑(f ↑x.1)) ∧ Bornology.IsBounded (Set.range fun x => ↑(f ↑x.1)) ↔
TauCeti.IsContinuousCompletelyMonotoneOnIoi f
Lean
Formalized in Tau Ceti as TauCeti.bcr_zero_spatial_iff_hausdorff_bernstein_widder.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.