PL1/RealSchur.lean

All source files · Download exact source

SHA-256: c85bc035b8a045dd06651a3f61a67a0a1fa3f87ddc872a8b7a49031e5d58b457

1import PL1.SchurExample2import Mathlib.Analysis.RCLike.Extend34/-!5# Weak convergence and the Schur property under restriction to real scalars67The full real and complex continuous duals induce the same sequential weak8convergence. The application uses the explicit restricted scalar action and9the inherited norm appearing in the reviewed theorem statements.10-/1112noncomputable section13open Filter14open scoped Topology1516namespace PL11718variable {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E]19variable [NormedSpace 𝕜 E] [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E]2021theorem weaklyConverges_iff_real {x : ℕ → E} {a : E} :22    WeaklyConverges 𝕜 E x a ↔ WeaklyConverges ℝ E x a := by23  constructor24  · intro hx φ25    have h := (RCLike.continuous_re.tendsto (StrongDual.extendRCLike (𝕜 := 𝕜) φ a)).comp26      (hx (StrongDual.extendRCLike (𝕜 := 𝕜) φ))27    simpa only [Function.comp_def, StrongDual.re_extendRCLike_apply] using h28  · intro hx φ29    have hr : Tendsto (fun n => RCLike.re (φ (x n))) atTop (𝓝 (RCLike.re (φ a))) :=30      hx (RCLike.reCLM.comp (φ.restrictScalars ℝ))31    have hi : Tendsto (fun n => RCLike.im (φ (x n))) atTop (𝓝 (RCLike.im (φ a))) :=32      hx (RCLike.imCLM.comp (φ.restrictScalars ℝ))33    have hr' := ((RCLike.continuous_ofReal : Continuous (fun r : ℝ => (r : 𝕜))).tendsto _).comp hr34    have hi' := ((RCLike.continuous_ofReal : Continuous (fun r : ℝ => (r : 𝕜))).tendsto _).comp hi35    simpa only [Function.comp_def, RCLike.re_add_im] using hr'.add (hi'.mul_const RCLike.I)3637theorem hasSchurProperty_iff_real : HasSchurProperty 𝕜 E ↔ HasSchurProperty ℝ E := by38  constructor39  · intro h x a hx40    exact h x a (weaklyConverges_iff_real.mpr hx)41  · intro h x a hx42    exact h x a (weaklyConverges_iff_real.mp hx)4344end PL14546namespace PL14748variable (𝕜 E : Type*) [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]4950/-- This statement spells out the inherited additive norm and restricted51real scalar action, so type-alias instance inference cannot select a different action. -/52theorem hasSchurProperty_iff_underlyingReal :53    HasSchurProperty 𝕜 E ↔54      @HasSchurProperty ℝ _ (UnderlyingReal 𝕜 E)55        (inferInstance : NormedAddCommGroup E) (NormedSpace.restrictScalars ℝ 𝕜 E) := by56  let : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E57  exact hasSchurProperty_iff_real5859theorem Noise.schurRates_projection_range_underlyingReal_hasSchurProperty :60    @HasSchurProperty ℝ _ (UnderlyingReal 𝕜 (Noise.projection 𝕜 Noise.schurRates).range)61      (inferInstance : NormedAddCommGroup (Noise.projection 𝕜 Noise.schurRates).range)62      (NormedSpace.restrictScalars ℝ 𝕜 (Noise.projection 𝕜 Noise.schurRates).range) :=63  (hasSchurProperty_iff_underlyingReal 𝕜 _).mp64    (Noise.schurRates_projection_range_hasSchurProperty 𝕜)6566end PL167