PL1/DaugavetAveraging.lean
All source files · Download exact source
SHA-256: 832e437f0790455c63080662464f16a66416a2c23c5e0d6197f163bc4cb6f8f0
1import PL1.DaugavetCriterion2import Mathlib.Analysis.Normed.Operator.NNNorm3import Mathlib.Topology.MetricSpace.Pseudo.Defs4import Mathlib.Tactic.FieldSimp5import Mathlib.Tactic.NormNum67/-!8# Finite averages of spikes imply the Daugavet slice criterion910All functionals are tested by finite averages. The only geometric input is11the explicitly stated finite-family hypothesis on a dense increasing union12of linear subspaces.13-/1415noncomputable section16open scoped BigOperators NNReal17namespace PL1.Daugavet1819variable (K E : Type*) [RCLike K] [NormedAddCommGroup E] [NormedSpace K E]2021/-- The quantitative finite spike family used in the manuscript. -/22def FiniteSpikeFamilies (V : ℕ → Submodule K E) : Prop :=23 ∀ n (h : E), h ∈ V n → ∀ f : E, f ∈ V n →24 ∀ δ : ℝ, 0 < δ → ∀ η : ℝ, 0 < η →25 ∃ N : ℕ, 0 < N ∧ ∃ w : Fin N → E,26 (N : K)⁻¹ • (∑ a, w a) = f ∧27 (∀ a, ‖w a‖ ≤ (1 + η) * ‖f‖) ∧28 (∀ a, (1 - 2 * δ) * (‖h‖ + ‖f‖) - η * ‖f‖ ≤ ‖h + w a‖)2930variable {K E}3132theorem exists_unit_re_apply_gt (φ : E →L[K] K) (hφ : ‖φ‖ = 1)33 {δ : ℝ} (hδ : 0 < δ) (hδ1 : δ < 1) :34 ∃ x : E, ‖x‖ = 1 ∧ 1 - δ < RCLike.re (φ x) := by35 obtain ⟨x, hx, hfx⟩ := φ.exists_nnnorm_eq_one_lt_apply_of_lt_opNNNorm36 (r := ⟨1 - δ, by linarith⟩) (by change 1 - δ < ‖φ‖; rw [hφ]; linarith)37 have hx' : ‖x‖ = 1 := congrArg (fun r : ℝ≥0 => (r : ℝ)) hx38 have hfx' : 1 - δ < ‖φ x‖ := hfx39 have hfx0 : φ x ≠ 0 := by40 intro he41 simp only [he, norm_zero] at hfx'42 linarith43 let c : K := (‖φ x‖ : K) / φ x44 have hc : ‖c‖ = 1 := by45 simp only [c, norm_div, RCLike.norm_ofReal, abs_norm]46 exact div_self (norm_ne_zero_iff.mpr hfx0)47 refine ⟨c • x, by rw [norm_smul, hc, hx', mul_one], ?_⟩48 simpa only [map_smul, smul_eq_mul, c, div_mul_cancel₀ _ hfx0, RCLike.ofReal_re] using hfx'4950theorem exists_unit_mem_dense_union (V : ℕ → Submodule K E)51 (hV : Dense (⋃ n, (V n : Set E))) (x : E) (hx : ‖x‖ = 1)52 {ε : ℝ} (hε : 0 < ε) :53 ∃ n, ∃ y : E, y ∈ V n ∧ ‖y‖ = 1 ∧ ‖x - y‖ < ε := by54 obtain ⟨v, hv, hxv⟩ := hV.exists_dist_lt x (lt_min (half_pos hε) (by norm_num : (0:ℝ)<1/2))55 obtain ⟨n, hvn⟩ := Set.mem_iUnion.mp hv56 rw [dist_eq_norm] at hxv57 have hv0 : v ≠ 0 := by58 intro he59 simp only [he, sub_zero, hx] at hxv60 linarith [min_le_right (ε / 2) (1 / 2 : ℝ)]61 have hvn0 : ‖v‖ ≠ 0 := norm_ne_zero_iff.mpr hv062 let y : E := ((‖v‖⁻¹ : ℝ) : K) • v63 have hy : ‖y‖ = 1 := by simp [y, norm_smul, inv_mul_cancel₀ hvn0]64 have hyv : (‖v‖ : K) • y = v := by65 dsimp only [y]66 rw [smul_smul, ← RCLike.ofReal_mul, mul_inv_cancel₀ hvn0, RCLike.ofReal_one, one_smul]67 have hdiff : v - y = ((‖v‖ - 1 : ℝ) : K) • y := by68 rw [RCLike.ofReal_sub, RCLike.ofReal_one, sub_smul, hyv, one_smul]69 have hnear : ‖v - y‖ ≤ ‖x - v‖ := by70 rw [hdiff, norm_smul, RCLike.norm_ofReal, hy, mul_one]71 simpa only [hx, norm_sub_rev] using abs_norm_sub_norm_le v x72 refine ⟨n, y, (V n).smul_mem _ hvn, hy, ?_⟩73 have ht := norm_add_le (x - v) (v - y)74 rw [sub_add_sub_cancel] at ht75 linarith [min_le_left (ε / 2) (1 / 2 : ℝ)]7677theorem exists_re_gt_of_finite_average (φ : E →L[K] K) {N : ℕ} (hN : 0 < N)78 (w : Fin N → E) (f : E) (hav : (N : K)⁻¹ • (∑ a, w a) = f)79 {b : ℝ} (hb : b < RCLike.re (φ f)) :80 ∃ a, b < RCLike.re (φ (w a)) := by81 classical82 have hNr : (0 : ℝ) < N := by exact_mod_cast hN83 have hc : (N : K)⁻¹ = (((N : ℝ)⁻¹ : ℝ) : K) := by simp84 have he := congrArg (fun x => RCLike.re (φ x)) hav85 simp only [map_smul, smul_eq_mul, hc, RCLike.mul_re, RCLike.ofReal_re,86 RCLike.ofReal_im, zero_mul, sub_zero, map_sum] at he87 by_contra! ha88 have hsum := Finset.sum_le_sum (fun a (_ : a ∈ Finset.univ) => ha a)89 simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] at hsum90 have hm := mul_le_mul_of_nonneg_left hsum (inv_nonneg.mpr hNr.le)91 rw [← mul_assoc, inv_mul_cancel₀ hNr.ne', one_mul, he] at hm92 linarith9394/-- The finite-average construction on a dense increasing union implies95the geometric slice criterion for every continuous dual functional. -/96theorem sliceCriterion_of_finiteSpikeFamilies (V : ℕ → Submodule K E)97 (hmono : Monotone V) (hdense : Dense (⋃ n, (V n : Set E)))98 (hspikes : FiniteSpikeFamilies K E V) : SliceCriterion K E := by99 classical100 intro h hh φ hφ ε hε101 let e : ℝ := min ε 1102 have he : 0 < e := lt_min hε zero_lt_one103 have heε : e ≤ ε := min_le_left _ _104 have he1 : e ≤ 1 := min_le_right _ _105 let d : ℝ := e / 64106 have hd : 0 < d := div_pos he (by norm_num)107 have hd1 : d < 1 := by dsimp [d]; linarith108 obtain ⟨g, hg, hφg⟩ := exists_unit_re_apply_gt φ hφ hd hd1109 obtain ⟨nf, f, hfV, hf, hgf⟩ := exists_unit_mem_dense_union V hdense g hg hd110 have hφf : 1 - 2 * d < RCLike.re (φ f) := by111 have hn := (RCLike.re_le_norm (φ (g - f))).trans (φ.le_opNorm (g - f))112 rw [map_sub, map_sub, hφ, one_mul] at hn113 linarith114 obtain ⟨nh, h₀, hhV, hh₀, hhh⟩ := exists_unit_mem_dense_union V hdense h hh hd115 obtain ⟨N, hN, w, hav, hw, hsep⟩ := hspikes (max nh nf) h₀116 (hmono (le_max_left _ _) hhV) f (hmono (le_max_right _ _) hfV) d hd d hd117 obtain ⟨a, ha⟩ := exists_re_gt_of_finite_average φ hN w f hav hφf118 let x : E := (((1 + d)⁻¹ : ℝ) : K) • w a119 have h1d : 0 < 1 + d := by linarith120 have hx : ‖x‖ ≤ 1 := by121 have hw' := hw a122 rw [hf, mul_one] at hw'123 dsimp [x]124 rw [norm_smul, RCLike.norm_ofReal, abs_of_pos (inv_pos.mpr h1d)]125 exact (mul_le_mul_of_nonneg_left hw' (inv_nonneg.mpr h1d.le)).trans_eq126 (inv_mul_cancel₀ h1d.ne')127 have hscale : ((1 + d : ℝ) : K) • x = w a := by128 dsimp only [x]129 rw [smul_smul, ← RCLike.ofReal_mul, mul_inv_cancel₀ h1d.ne', RCLike.ofReal_one, one_smul]130 have hdiff : w a - x = (d : K) • x := by131 rw [← hscale, RCLike.ofReal_add, RCLike.ofReal_one, add_smul, one_smul]132 abel133 have hdiffnorm : ‖w a - x‖ ≤ d := by134 rw [hdiff, norm_smul, RCLike.norm_ofReal, abs_of_pos hd]135 exact mul_le_of_le_one_right hd.le hx136 have hφx : (1 + d) * RCLike.re (φ x) = RCLike.re (φ (w a)) := by137 have hs := congrArg (fun v => RCLike.re (φ v)) hscale138 simpa only [map_smul, smul_eq_mul, RCLike.mul_re, RCLike.ofReal_re,139 RCLike.ofReal_im, zero_mul, sub_zero] using hs140 refine ⟨x, hx, ?_, ?_⟩141 · have hreal : 1 - ε < (1 - 2 * d) / (1 + d) := by142 apply (lt_div_iff₀ h1d).mpr143 have heq : e = 64 * d := by dsimp [d]; ring144 nlinarith [mul_nonneg hε.le hd.le]145 exact hreal.trans ((div_lt_iff₀ h1d).mpr (by nlinarith [ha]))146 · have hs := hsep a147 rw [hh₀, hf] at hs148 have htri := norm_sub_norm_le (h₀ + w a) (h + x)149 have hid : (h₀ + w a) - (h + x) = (h₀ - h) + (w a - x) := by abel150 rw [hid] at htri151 have hu := norm_add_le (h₀ - h) (w a - x)152 rw [norm_sub_rev h₀ h] at hu153 have heq : e = 64 * d := by dsimp [d]; ring154 nlinarith155156end PL1.Daugavet157