PL1/DaugavetCriterion.lean
All source files · Download exact source
SHA-256: 3d71f8de270866b9cab3fdb0eecc0b33d82d879b4ca8798504838148f76c21f0
1import Mathlib.Analysis.Normed.Operator.NormedSpace2import Mathlib.Analysis.RCLike.Basic3import Mathlib.Tactic.Linarith4import Mathlib.Tactic.Ring5import Mathlib.Tactic.Abel67/-! # The Daugavet slice criterion over the real and complex scalar fields89The geometric slice condition implies the norm identity for every bounded10rank-one operator. Rank-one maps are written as `φ.smulRight y`.11-/1213noncomputable section14namespace PL1.Daugavet1516variable {𝕜 : Type*} [RCLike 𝕜]17variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]1819/-- The usual geometric criterion, phrased with real parts for either scalar field. -/20def SliceCriterion (𝕜 E : Type*) [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Prop :=21 ∀ h : E, ‖h‖ = 1 → ∀ φ : E →L[𝕜] 𝕜, ‖φ‖ = 1 → ∀ ε : ℝ, 0 < ε →22 ∃ x : E, ‖x‖ ≤ 1 ∧ 1 - ε < RCLike.re (φ x) ∧ 2 - ε < ‖h + x‖2324/-- The Daugavet norm identity for the actual bounded rank-one maps. -/25def HasDaugavetProperty (𝕜 E : Type*) [RCLike 𝕜] [NormedAddCommGroup E]26 [NormedSpace 𝕜 E] : Prop :=27 ∀ (φ : E →L[𝕜] 𝕜) (y : E),28 ‖ContinuousLinearMap.id 𝕜 E + φ.smulRight y‖ = 1 + ‖φ.smulRight y‖2930private theorem norm_sub_one_lt (z : 𝕜) (hz : ‖z‖ ≤ 1) (ε δ : ℝ)31 (hε : 0 < ε) (hδ : δ ≤ ε ^ 2 / 2) (hre : 1 - δ < RCLike.re z) : ‖z - 1‖ < ε := by32 have hs : ‖z - 1‖ ^ 2 = ‖z‖ ^ 2 + 1 - 2 * RCLike.re z := by33 simpa only [RCLike.normSq_eq_def', norm_one, one_pow, map_one, mul_one] using34 RCLike.normSq_sub z 135 have hzn := norm_nonneg z36 have hdn := norm_nonneg (z - 1)37 nlinarith3839/-- A sufficiently thin real-part slice also controls the complex phase. -/40theorem SliceCriterion.exists_near_one (hs : SliceCriterion 𝕜 E)41 (h : E) (hh : ‖h‖ = 1) (φ : E →L[𝕜] 𝕜) (hφ : ‖φ‖ = 1)42 (ε : ℝ) (hε : 0 < ε) :43 ∃ x : E, ‖x‖ ≤ 1 ∧ ‖φ x - 1‖ < ε ∧ 2 - ε < ‖h + x‖ := by44 let δ := min ε (ε ^ 2 / 2)45 have hδ : 0 < δ := lt_min hε (by positivity)46 obtain ⟨x, hx, hφx, hsum⟩ := hs h hh φ hφ δ hδ47 refine ⟨x, hx, norm_sub_one_lt (φ x) ?_ ε δ hε (min_le_right _ _) hφx, ?_⟩48 · exact (φ.le_opNorm x).trans (by simpa only [hφ, one_mul] using hx)49 · exact lt_of_le_of_lt (by dsimp [δ]; linarith [min_le_left ε (ε ^ 2 / 2)]) hsum5051private theorem weighted_separation (h x : E) (hh : ‖h‖ = 1) (hx : ‖x‖ ≤ 1)52 (ε t : ℝ) (hε : 0 < ε) (ht : 0 ≤ t) (hs : 2 - ε < ‖h + x‖) :53 1 + t - (1 + t) * ε < ‖x + (t : 𝕜) • h‖ := by54 by_cases ht1 : t ≤ 155 · have he : x + h = (x + (t : 𝕜) • h) + ((1 - t : ℝ) : 𝕜) • h := by56 simp only [RCLike.ofReal_sub, RCLike.ofReal_one, sub_smul, one_smul]57 abel58 have hn := norm_add_le (x + (t : 𝕜) • h) (((1 - t : ℝ) : 𝕜) • h)59 rw [← he, norm_smul, RCLike.norm_ofReal, abs_of_nonneg (sub_nonneg.mpr ht1), hh, mul_one] at hn60 rw [add_comm h x] at hs61 nlinarith [mul_nonneg ht hε.le]62 · have ht1' : 1 ≤ t := le_of_lt (lt_of_not_ge ht1)63 have he : (t : 𝕜) • (x + h) =64 (x + (t : 𝕜) • h) + ((t - 1 : ℝ) : 𝕜) • x := by65 simp only [smul_add, RCLike.ofReal_sub, RCLike.ofReal_one, sub_smul, one_smul]66 abel67 have hn := norm_add_le (x + (t : 𝕜) • h) (((t - 1 : ℝ) : 𝕜) • x)68 rw [← he, norm_smul, norm_smul, RCLike.norm_ofReal, RCLike.norm_ofReal,69 abs_of_nonneg ht, abs_of_nonneg (sub_nonneg.mpr ht1')] at hn70 rw [add_comm h x] at hs71 have hm := mul_lt_mul_of_pos_left hs (show 0 < t by linarith)72 have hx' := mul_le_mul_of_nonneg_left hx (sub_nonneg.mpr ht1')73 nlinarith7475private theorem norm_id_add_scaled_rankOne [Nontrivial E]76 (hs : SliceCriterion 𝕜 E) (h : E) (hh : ‖h‖ = 1)77 (φ : E →L[𝕜] 𝕜) (hφ : ‖φ‖ = 1) (t : ℝ) (ht : 0 ≤ t) :78 ‖ContinuousLinearMap.id 𝕜 E + (t : 𝕜) • φ.smulRight h‖ = 1 + t := by79 let T : E →L[𝕜] E := ContinuousLinearMap.id 𝕜 E + (t : 𝕜) • φ.smulRight h80 have hupper : ‖T‖ ≤ 1 + t := by81 calc82 _ ≤ ‖ContinuousLinearMap.id 𝕜 E‖ + ‖(t : 𝕜) • φ.smulRight h‖ := norm_add_le _ _83 _ = _ := by simp [norm_smul, abs_of_nonneg ht,84 ContinuousLinearMap.norm_smulRight_apply, hφ, hh]85 have hlower (ε : ℝ) (hε : 0 < ε) : 1 + t - ε < ‖T‖ := by86 let δ := ε / (1 + 2 * t)87 have hd : 0 < δ := div_pos hε (by linarith)88 obtain ⟨x, hx, hφx, hsum⟩ := hs.exists_near_one h hh φ hφ δ hd89 have hw := weighted_separation (𝕜 := 𝕜) h x hh hx δ t hd ht hsum90 have he : (x + (t : 𝕜) • h) - T x = -((t : 𝕜) • ((φ x - 1) • h)) := by91 simp only [T, add_apply, ContinuousLinearMap.id_apply,92 smul_apply, ContinuousLinearMap.smulRight_apply,93 sub_smul, smul_sub, one_smul]94 abel95 have hn := norm_sub_norm_le (x + (t : 𝕜) • h) (T x)96 rw [he, norm_neg, norm_smul, norm_smul, RCLike.norm_ofReal,97 abs_of_nonneg ht, hh, mul_one] at hn98 have hm := mul_le_mul_of_nonneg_left hφx.le ht99 have hTx : ‖T x‖ ≤ ‖T‖ :=100 (T.le_opNorm x).trans (mul_le_of_le_one_right (norm_nonneg T) hx)101 have hδeq : (1 + 2 * t) * δ = ε := by102 dsimp [δ]103 field_simp104 nlinarith105 apply le_antisymm hupper106 by_contra hn107 have he : 0 < (1 + t - ‖T‖) / 2 := by linarith108 have h := hlower ((1 + t - ‖T‖) / 2) he109 linarith110111/-- The geometric slice criterion implies the Daugavet norm equation for every rank-one map. -/112theorem SliceCriterion.hasDaugavetProperty [Nontrivial E] (hs : SliceCriterion 𝕜 E) :113 HasDaugavetProperty 𝕜 E := by114 intro φ y115 by_cases hφ : φ = 0116 · simp [hφ]117 by_cases hy : y = 0118 · simp [hy]119 have hφn : ‖φ‖ ≠ 0 := norm_ne_zero_iff.mpr hφ120 have hyn : ‖y‖ ≠ 0 := norm_ne_zero_iff.mpr hy121 let ψ : E →L[𝕜] 𝕜 := ((‖φ‖⁻¹ : ℝ) : 𝕜) • φ122 let h : E := ((‖y‖⁻¹ : ℝ) : 𝕜) • y123 have hψ : ‖ψ‖ = 1 := by124 simp [ψ, norm_smul,125 inv_mul_cancel₀ hφn]126 have hh : ‖h‖ = 1 := by127 simp [h, norm_smul,128 inv_mul_cancel₀ hyn]129 have hφK : (‖φ‖ : 𝕜) ≠ 0 := by exact_mod_cast hφn130 have hyK : (‖y‖ : 𝕜) ≠ 0 := by exact_mod_cast hyn131 have he : (((‖φ‖ * ‖y‖ : ℝ) : 𝕜) • ψ.smulRight h) = φ.smulRight y := by132 ext x133 simp only [ψ, h, smul_apply, ContinuousLinearMap.smulRight_apply,134 smul_smul, smul_eq_mul, RCLike.ofReal_mul, RCLike.ofReal_inv]135 congr 1136 field_simp137 have hn := norm_id_add_scaled_rankOne hs h hh ψ hψ (‖φ‖ * ‖y‖)138 (mul_nonneg (norm_nonneg _) (norm_nonneg _))139 rw [he] at hn140 simpa only [ContinuousLinearMap.norm_smulRight_apply] using hn141142#print axioms SliceCriterion.hasDaugavetProperty143144end PL1.Daugavet145