PL1/DaugavetDiameter.lean
All source files · Download exact source
SHA-256: 3830ccf2995e4aee967c284f61ccaedab791b688985c0918215d5398197f140d
1import PL1.DaugavetRealification2import PL1.IntrinsicExposedPoint3import Mathlib.Topology.MetricSpace.Bounded45/-!6# Diameter two for slices of the actual intrinsic unit balls78The slice criterion gives points almost distance two apart in each normalized9real-part slice. All intrinsic specializations retain the original graph norm.10The underlying-real statements quantify over the full real continuous dual.11-/1213noncomputable section14open Filter15open scoped Topology1617namespace PL1.Daugavet1819variable {K E : Type*} [RCLike K] [NormedAddCommGroup E] [NormedSpace K E]2021/-- A real-part slice of the closed unit ball; normalization and positive22thickness are explicit hypotheses of the theorems below. -/23def realPartSlice (φ : E →L[K] K) (α : ℝ) : Set E :=24 {x | ‖x‖ ≤ 1 ∧ 1 - α < RCLike.re (φ x)}2526theorem dist_le_two_of_mem_realPartSlice {φ : E →L[K] K} {α : ℝ}27 {x y : E} (hx : x ∈ realPartSlice φ α) (hy : y ∈ realPartSlice φ α) :28 dist x y ≤ 2 := by29 rw [dist_eq_norm]30 have hn := norm_sub_le x y31 linarith [hx.1, hy.1]3233theorem isBounded_realPartSlice (φ : E →L[K] K) (α : ℝ) :34 Bornology.IsBounded (realPartSlice φ α) :=35 Metric.isBounded_iff.mpr ⟨2, fun _ hx _ hy => dist_le_two_of_mem_realPartSlice hx hy⟩3637/-- Every prescribed unit vector has points almost distance two away inside38any normalized real-part slice. -/39theorem SliceCriterion.exists_far_in_realPartSlice (hs : SliceCriterion K E)40 (φ : E →L[K] K) (hφ : ‖φ‖ = 1) {α ε : ℝ} (hα : 0 < α) (hε : 0 < ε)41 (x : E) (hx : ‖x‖ = 1) :42 ∃ y ∈ realPartSlice φ α, 2 - ε < dist x y := by43 obtain ⟨y, hy, hφy, hxy⟩ := hs (-x) (by simpa only [norm_neg] using hx)44 φ hφ (min α ε) (lt_min hα hε)45 refine ⟨y, ⟨hy, ?_⟩, ?_⟩46 · exact lt_of_le_of_lt (by linarith [min_le_left α ε]) hφy47 · have hn : dist x y = ‖-x + y‖ := by48 rw [dist_eq_norm, norm_sub_rev, sub_eq_add_neg, add_comm]49 rw [hn]50 exact lt_of_le_of_lt (by linarith [min_le_right α ε]) hxy5152/-- Explicit pairs in each normalized slice approach the maximum distance two. -/53theorem SliceCriterion.exists_dist_gt_in_realPartSlice (hs : SliceCriterion K E)54 (φ : E →L[K] K) (hφ : ‖φ‖ = 1) {α ε : ℝ} (hα : 0 < α) (hε : 0 < ε) :55 ∃ x ∈ realPartSlice φ α, ∃ y ∈ realPartSlice φ α, 2 - ε < dist x y := by56 obtain ⟨x, hx, hφx⟩ := exists_unit_re_apply_gt φ hφ57 (lt_min (half_pos hα) (by norm_num : (0 : ℝ) < 1 / 2))58 (lt_of_le_of_lt (min_le_right (α / 2) (1 / 2)) (by norm_num))59 obtain ⟨y, hy, hxy⟩ := hs.exists_far_in_realPartSlice φ hφ hα hε x hx60 exact ⟨x, ⟨hx.le, lt_of_le_of_lt (by linarith [min_le_left (α / 2) (1 / 2)]) hφx⟩,61 y, hy, hxy⟩6263/-- Each normalized real-part slice of the closed unit ball has diameter exactly two. -/64theorem SliceCriterion.diam_realPartSlice (hs : SliceCriterion K E)65 (φ : E →L[K] K) (hφ : ‖φ‖ = 1) {α : ℝ} (hα : 0 < α) :66 Metric.diam (realPartSlice φ α) = 2 := by67 apply le_antisymm68 · exact Metric.diam_le_of_forall_dist_le (by norm_num)69 (fun _ hx _ hy => dist_le_two_of_mem_realPartSlice hx hy)70 · by_contra! hlt71 obtain ⟨x, hx, y, hy, hxy⟩ := hs.exists_dist_gt_in_realPartSlice φ hφ hα72 (sub_pos.mpr hlt)73 have hd := Metric.dist_le_diam_of_mem (isBounded_realPartSlice φ α) hx hy74 linarith7576/-- Every normalized real-part slice has metric diameter two. -/77def SliceDiameterTwo (K E : Type*) [RCLike K] [NormedAddCommGroup E]78 [NormedSpace K E] : Prop :=79 ∀ (φ : E →L[K] K), ‖φ‖ = 1 → ∀ {α : ℝ}, 0 < α →80 Metric.diam (realPartSlice φ α) = 28182theorem SliceCriterion.sliceDiameterTwo (hs : SliceCriterion K E) : SliceDiameterTwo K E :=83 fun φ hφ _ hα => hs.diam_realPartSlice φ hφ hα8485/-- Maximizing sequences can remain asymptotically distance two from any86prescribed unit vector. In particular, a maximizer cannot be strongly exposed. -/87theorem SliceCriterion.exists_maximizing_sequence_far (hs : SliceCriterion K E)88 (φ : E →L[K] K) (hφ : ‖φ‖ = 1) (x : E) (hx : ‖x‖ = 1) :89 ∃ y : ℕ → E, (∀ n, ‖y n‖ ≤ 1) ∧90 Tendsto (fun n => RCLike.re (φ (y n))) atTop (𝓝 1) ∧91 Tendsto (fun n => dist x (y n)) atTop (𝓝 2) ∧92 ¬ Tendsto y atTop (𝓝 x) := by93 have hex (n : ℕ) : ∃ y ∈ realPartSlice φ (1 / ((n : ℝ) + 1)),94 2 - 1 / ((n : ℝ) + 1) < dist x y :=95 hs.exists_far_in_realPartSlice φ hφ (by positivity) (by positivity) x hx96 choose y hy hd using hex97 have hupper (n : ℕ) : RCLike.re (φ (y n)) ≤ 1 :=98 (RCLike.re_le_norm _).trans ((φ.le_opNorm _).trans (by simpa only [hφ, one_mul] using (hy n).1))99 have hinv : Tendsto (fun n : ℕ => 1 / ((n : ℝ) + 1)) atTop (𝓝 0) :=100 tendsto_one_div_add_atTop_nhds_zero_nat101 have hre : Tendsto (fun n => RCLike.re (φ (y n))) atTop (𝓝 1) :=102 tendsto_of_tendsto_of_tendsto_of_le_of_le103 (by simpa only [sub_zero] using tendsto_const_nhds.sub hinv)104 tendsto_const_nhds (fun n => (hy n).2.le) hupper105 have hdist : Tendsto (fun n => dist x (y n)) atTop (𝓝 2) := by106 apply tendsto_of_tendsto_of_tendsto_of_le_of_le107 (by simpa only [sub_zero] using tendsto_const_nhds.sub hinv) tendsto_const_nhds108 (fun n => (hd n).le)109 intro n110 change dist x (y n) ≤ 2111 rw [dist_eq_norm]112 have hn := norm_sub_le x (y n)113 linarith [(hy n).1]114 refine ⟨y, fun n => (hy n).1, hre, hdist, ?_⟩115 intro hconv116 have hzero : Tendsto (fun n => dist x (y n)) atTop (𝓝 0) := by117 simpa only [dist_self] using (tendsto_const_nhds (x := x)).dist hconv118 have h02 : (0 : ℝ) = 2 := tendsto_nhds_unique hzero hdist119 norm_num at h02120121/-- The sequential property required for strong exposure fails for every122normalized functional and every unit vector. -/123theorem SliceCriterion.not_strongly_exposes (hs : SliceCriterion K E)124 (φ : E →L[K] K) (hφ : ‖φ‖ = 1) (x : E) (hx : ‖x‖ = 1) :125 ¬ (∀ y : ℕ → E, (∀ n, ‖y n‖ ≤ 1) →126 Tendsto (fun n => RCLike.re (φ (y n))) atTop (𝓝 1) → Tendsto y atTop (𝓝 x)) := by127 obtain ⟨y, hy, hre, _, hnot⟩ := hs.exists_maximizing_sequence_far φ hφ x hx128 exact fun h => hnot (h y hy hre)129130end PL1.Daugavet131132namespace PL1.Noise133134variable (K : Type*) [RCLike K]135136/-- Diameter two in every scalar-dual slice of the Schur intrinsic unit ball. -/137theorem schur_intrinsic_diam_realPartSlice138 (φ : (dyadicSystem K schurRates).IntrinsicSpace →L[K] K)139 (hφ : ‖φ‖ = 1) {α : ℝ} (hα : 0 < α) :140 Metric.diam (Daugavet.realPartSlice φ α) = 2 :=141 (schur_intrinsic_sliceCriterion K).diam_realPartSlice φ hφ hα142143/-- Diameter two in every scalar-dual slice of the constant-rate intrinsic unit ball. -/144theorem constant_intrinsic_diam_realPartSlice145 (φ : (dyadicSystem K constantRates).IntrinsicSpace →L[K] K)146 (hφ : ‖φ‖ = 1) {α : ℝ} (hα : 0 < α) :147 Metric.diam (Daugavet.realPartSlice φ α) = 2 :=148 (constant_intrinsic_sliceCriterion K).diam_realPartSlice φ hφ hα149150/-- The same diameter statement for every real-linear functional, using the151original norm of the Schur intrinsic space. -/152theorem schur_intrinsic_underlyingReal_diam_realPartSlice :153 @Daugavet.SliceDiameterTwo ℝ154 (UnderlyingReal K (dyadicSystem K schurRates).IntrinsicSpace) _155 (inferInstance : NormedAddCommGroup (dyadicSystem K schurRates).IntrinsicSpace)156 (NormedSpace.restrictScalars ℝ K (dyadicSystem K schurRates).IntrinsicSpace) :=157 @Daugavet.SliceCriterion.sliceDiameterTwo ℝ158 (UnderlyingReal K (dyadicSystem K schurRates).IntrinsicSpace) _159 (inferInstance : NormedAddCommGroup (dyadicSystem K schurRates).IntrinsicSpace)160 (NormedSpace.restrictScalars ℝ K (dyadicSystem K schurRates).IntrinsicSpace)161 (schur_intrinsic_underlyingReal_sliceCriterion K)162163/-- Diameter two for every real-linear functional on the constant-rate space. -/164theorem constant_intrinsic_underlyingReal_diam_realPartSlice :165 @Daugavet.SliceDiameterTwo ℝ166 (UnderlyingReal K (dyadicSystem K constantRates).IntrinsicSpace) _167 (inferInstance : NormedAddCommGroup (dyadicSystem K constantRates).IntrinsicSpace)168 (NormedSpace.restrictScalars ℝ K (dyadicSystem K constantRates).IntrinsicSpace) :=169 @Daugavet.SliceCriterion.sliceDiameterTwo ℝ170 (UnderlyingReal K (dyadicSystem K constantRates).IntrinsicSpace) _171 (inferInstance : NormedAddCommGroup (dyadicSystem K constantRates).IntrinsicSpace)172 (NormedSpace.restrictScalars ℝ K (dyadicSystem K constantRates).IntrinsicSpace)173 (constant_intrinsic_underlyingReal_sliceCriterion K)174175/-- The functional exposing `1` on the Schur intrinsic ball admits maximizing176sequences at asymptotic distance two from that constant. -/177theorem schur_intrinsic_integral_maximizing_sequence_far :178 ∃ y : ℕ → (dyadicSystem K schurRates).IntrinsicSpace,179 (∀ n, ‖y n‖ ≤ 1) ∧180 Tendsto (fun n => RCLike.re (IntrinsicExposedPoint.integralFunctional K schurRates (y n)))181 atTop (𝓝 1) ∧182 Tendsto (fun n => dist (intrinsicCharacter K schurRates ∅) (y n)) atTop (𝓝 2) ∧183 ¬ Tendsto y atTop (𝓝 (intrinsicCharacter K schurRates ∅)) :=184 (schur_intrinsic_sliceCriterion K).exists_maximizing_sequence_far185 (IntrinsicExposedPoint.integralFunctional K schurRates)186 (IntrinsicExposedPoint.norm_integralFunctional K schurRates)187 (intrinsicCharacter K schurRates ∅) (IntrinsicTailNorm.norm_intrinsicConstant K schurRates)188189/-- The same explicit failure of strong exposure in the constant-rate space. -/190theorem constant_intrinsic_integral_maximizing_sequence_far :191 ∃ y : ℕ → (dyadicSystem K constantRates).IntrinsicSpace,192 (∀ n, ‖y n‖ ≤ 1) ∧193 Tendsto (fun n => RCLike.re (IntrinsicExposedPoint.integralFunctional K constantRates (y n)))194 atTop (𝓝 1) ∧195 Tendsto (fun n => dist (intrinsicCharacter K constantRates ∅) (y n)) atTop (𝓝 2) ∧196 ¬ Tendsto y atTop (𝓝 (intrinsicCharacter K constantRates ∅)) :=197 (constant_intrinsic_sliceCriterion K).exists_maximizing_sequence_far198 (IntrinsicExposedPoint.integralFunctional K constantRates)199 (IntrinsicExposedPoint.norm_integralFunctional K constantRates)200 (intrinsicCharacter K constantRates ∅) (IntrinsicTailNorm.norm_intrinsicConstant K constantRates)201202end PL1.Noise203