PL1/DaugavetRealification.lean

All source files · Download exact source

SHA-256: a530f1cc9e02bde29714e6e77ed83382159769693c8b9c897d4c01b4eb0ca925

1import PL1.MainDaugavet23/-! # Daugavet for all real rank-one operators on the same intrinsic norm45Finite spike families use real coefficients in their averages. They survive6restriction of scalars, so the real slice criterion tests the entire real7continuous dual, including functionals that are not complex linear.8-/910noncomputable section11open scoped NNReal BigOperators12namespace PL1.Daugavet1314variable {K E : Type*} [RCLike K] [NormedAddCommGroup E]15  [NormedSpace K E] [NormedSpace ℝ E] [IsScalarTower ℝ K E]1617/-- Restricting a finite spike family to real scalars preserves its exact averages and norms. -/18theorem FiniteSpikeFamilies.restrictScalars {V : ℕ → Submodule K E}19    (hspikes : FiniteSpikeFamilies K E V) :20    FiniteSpikeFamilies ℝ E (fun n => (V n).restrictScalars ℝ) := by21  intro n h hh f hf δ hδ η hη22  obtain ⟨N, hN, w, hav, hnorm, hsep⟩ := hspikes n h hh f hf δ hδ η hη23  refine ⟨N, hN, w, ?_, hnorm, hsep⟩24  rw [RCLike.real_smul_eq_coe_smul (K := K)]25  simpa only [RCLike.ofReal_inv, RCLike.ofReal_natCast] using hav2627/-- Monotonicity and density of the original subspaces give the full real slice criterion. -/28theorem real_sliceCriterion_of_finiteSpikeFamilies (V : ℕ → Submodule K E)29    (hmono : Monotone V) (hdense : Dense (⋃ n, (V n : Set E)))30    (hspikes : FiniteSpikeFamilies K E V) : SliceCriterion ℝ E :=31  sliceCriterion_of_finiteSpikeFamilies (fun n => (V n).restrictScalars ℝ)32    (fun _ _ hnm => hmono hnm) hdense hspikes.restrictScalars3334/-- This statement explicitly retains the original additive norm and restricted real action. -/35theorem underlyingReal_sliceCriterion_of_finiteSpikeFamilies36    {K E : Type*} [RCLike K] [NormedAddCommGroup E] [NormedSpace K E]37    (V : ℕ → Submodule K E) (hmono : Monotone V)38    (hdense : Dense (⋃ n, (V n : Set E))) (hspikes : FiniteSpikeFamilies K E V) :39    @SliceCriterion ℝ (UnderlyingReal K E) _40      (inferInstance : NormedAddCommGroup E) (NormedSpace.restrictScalars ℝ K E) := by41  let : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ K E42  exact real_sliceCriterion_of_finiteSpikeFamilies (K := K) (E := E) V hmono hdense hspikes4344end PL1.Daugavet4546namespace PL1.Noise47variable (K : Type*) [RCLike K]4849/-- The Schur construction satisfies every real slice test with the original graph norm. -/50theorem schur_intrinsic_underlyingReal_sliceCriterion :51    @Daugavet.SliceCriterion ℝ (UnderlyingReal K (dyadicSystem K schurRates).IntrinsicSpace) _52      (inferInstance : NormedAddCommGroup (dyadicSystem K schurRates).IntrinsicSpace)53      (NormedSpace.restrictScalars ℝ K (dyadicSystem K schurRates).IntrinsicSpace) :=54  Daugavet.underlyingReal_sliceCriterion_of_finiteSpikeFamilies55    (fun n => (intrinsicExpectation K schurRates n).range)56    (intrinsicExpectation_range_monotone K schurRates)57    (dense_iUnion_intrinsicExpectation_range K schurRates)58    (IntrinsicSpikeFamilies.finiteSpikeFamilies schurRates59      (fun d T _ hδ => TailSpikes.exists_family d T hδ))6061/-- The constant-rate construction satisfies the same full real slice criterion. -/62theorem constant_intrinsic_underlyingReal_sliceCriterion :63    @Daugavet.SliceCriterion ℝ (UnderlyingReal K (dyadicSystem K constantRates).IntrinsicSpace) _64      (inferInstance : NormedAddCommGroup (dyadicSystem K constantRates).IntrinsicSpace)65      (NormedSpace.restrictScalars ℝ K (dyadicSystem K constantRates).IntrinsicSpace) :=66  Daugavet.underlyingReal_sliceCriterion_of_finiteSpikeFamilies67    (fun n => (intrinsicExpectation K constantRates n).range)68    (intrinsicExpectation_range_monotone K constantRates)69    (dense_iUnion_intrinsicExpectation_range K constantRates)70    (IntrinsicSpikeFamilies.finiteSpikeFamilies constantRates71      (fun d T _ hδ => TailSpikes.exists_constant_family d T hδ))7273/-- All real rank-one operators satisfy the Daugavet equation on the Schur intrinsic space. -/74theorem schur_intrinsic_underlyingReal_hasDaugavetProperty :75    @Daugavet.HasDaugavetProperty ℝ (UnderlyingReal K (dyadicSystem K schurRates).IntrinsicSpace) _76      (inferInstance : NormedAddCommGroup (dyadicSystem K schurRates).IntrinsicSpace)77      (NormedSpace.restrictScalars ℝ K (dyadicSystem K schurRates).IntrinsicSpace) := by78  let := intrinsicSpace_nontrivial K schurRates79  let : NormedSpace ℝ (dyadicSystem K schurRates).IntrinsicSpace :=80    NormedSpace.restrictScalars ℝ K (dyadicSystem K schurRates).IntrinsicSpace81  exact Daugavet.SliceCriterion.hasDaugavetProperty (𝕜 := ℝ) (E := (dyadicSystem K schurRates).IntrinsicSpace) (schur_intrinsic_underlyingReal_sliceCriterion K)8283/-- All real rank-one operators satisfy the Daugavet equation on the constant-rate intrinsic space. -/84theorem constant_intrinsic_underlyingReal_hasDaugavetProperty :85    @Daugavet.HasDaugavetProperty ℝ (UnderlyingReal K (dyadicSystem K constantRates).IntrinsicSpace) _86      (inferInstance : NormedAddCommGroup (dyadicSystem K constantRates).IntrinsicSpace)87      (NormedSpace.restrictScalars ℝ K (dyadicSystem K constantRates).IntrinsicSpace) := by88  let := intrinsicSpace_nontrivial K constantRates89  let : NormedSpace ℝ (dyadicSystem K constantRates).IntrinsicSpace :=90    NormedSpace.restrictScalars ℝ K (dyadicSystem K constantRates).IntrinsicSpace91  exact Daugavet.SliceCriterion.hasDaugavetProperty (𝕜 := ℝ) (E := (dyadicSystem K constantRates).IntrinsicSpace) (constant_intrinsic_underlyingReal_sliceCriterion K)9293#print axioms schur_intrinsic_underlyingReal_hasDaugavetProperty94#print axioms constant_intrinsic_underlyingReal_hasDaugavetProperty95end PL1.Noise96