PL1/IntrinsicSpikeEstimates.lean
All source files · Download exact source
SHA-256: 1c829607852e4c52da7006f92ca1e5e93729b2918e5a4731e8ad0ad5d1e67343
1import PL1.IntrinsicGraph23/-!4# Summable coordinate estimates for actual intrinsic products56The multiplication map is an actual continuous linear operator on the base7space. Coordinate norm identities and commutator estimates remain explicit8inputs here; the conclusions concern the original intrinsic graph and norm.9-/1011noncomputable section12open scoped BigOperators1314namespace PL1.IntrinsicSpikeEstimates15open IntrinsicGraph1617variable {𝕜 Y : Type*} [RCLike 𝕜]18 [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]19 {D : ℕ → Y →L[𝕜] Y}2021theorem summable_norm_coord (f : Space D) : Summable (fun n => ‖coord D n f‖) := by22 simpa only [coord_apply, ENNReal.toReal_one, Real.rpow_one] using23 (lp.memℓp (f : Ambient (Y := Y))).summable (by norm_num)2425theorem summable_product_coordinates (M : Y →L[𝕜] Y) (f : Space D)26 (e : ℕ → ℝ) (he : Summable e)27 (hpres : ∀ n, ‖M (coord D n f)‖ = ‖coord D n f‖)28 (hcomm : ∀ n, ‖D n (M (evalZero D f)) - M (coord D n f)‖ ≤ e n) :29 Summable (fun n => ‖D n (M (evalZero D f))‖) := by30 apply Summable.of_nonneg_of_le (fun _ => norm_nonneg _)31 (fun n => ?_) ((summable_norm_coord f).add he)32 calc33 ‖D n (M (evalZero D f))‖ ≤34 ‖D n (M (evalZero D f)) - M (coord D n f)‖ + ‖M (coord D n f)‖ :=35 norm_le_norm_sub_add _ _36 _ ≤ e n + ‖coord D n f‖ := by rw [hpres]; exact add_le_add (hcomm n) le_rfl37 _ = ‖coord D n f‖ + e n := add_comm _ _3839theorem norm_product_sub_norm_le (M : Y →L[𝕜] Y) (f g : Space D)40 (hg : evalZero D g = M (evalZero D f)) (e : ℕ → ℝ) (he : Summable e)41 (hpres : ∀ n, ‖M (coord D n f)‖ = ‖coord D n f‖)42 (hcomm : ∀ n, ‖D n (M (evalZero D f)) - M (coord D n f)‖ ≤ e n) :43 |‖g‖ - ‖f‖| ≤ ∑' n, e n := by44 have hcoord (n : ℕ) : ‖coord D n g - M (coord D n f)‖ ≤ e n := by45 rw [coord_eq, hg]46 exact hcomm n47 have hupper : ‖g‖ ≤ ‖f‖ + ∑' n, e n := by48 rw [norm_eq_tsum, norm_eq_tsum, ← (summable_norm_coord f).tsum_add he]49 apply (summable_norm_coord g).tsum_le_tsum _ ((summable_norm_coord f).add he)50 intro n51 calc52 ‖coord D n g‖ ≤ ‖coord D n g - M (coord D n f)‖ + ‖M (coord D n f)‖ :=53 norm_le_norm_sub_add _ _54 _ ≤ ‖coord D n f‖ + e n := by rw [hpres]; linarith [hcoord n]55 have hlower : ‖f‖ ≤ ‖g‖ + ∑' n, e n := by56 rw [norm_eq_tsum, norm_eq_tsum, ← (summable_norm_coord g).tsum_add he]57 apply (summable_norm_coord f).tsum_le_tsum _ ((summable_norm_coord g).add he)58 intro n59 calc60 ‖coord D n f‖ = ‖M (coord D n f)‖ := (hpres n).symm61 _ ≤ ‖M (coord D n f) - coord D n g‖ + ‖coord D n g‖ :=62 norm_le_norm_sub_add _ _63 _ ≤ ‖coord D n g‖ + e n := by rw [norm_sub_rev]; linarith [hcoord n]64 exact abs_le.mpr ⟨by linarith, by linarith⟩6566/-- Norm summability constructs the product in the actual graph, not in a new67space with a modified norm. -/68theorem exists_product (h0 : D 0 = ContinuousLinearMap.id 𝕜 Y)69 (M : Y →L[𝕜] Y) (f : Space D) (e : ℕ → ℝ) (he : Summable e)70 (hpres : ∀ n, ‖M (coord D n f)‖ = ‖coord D n f‖)71 (hcomm : ∀ n, ‖D n (M (evalZero D f)) - M (coord D n f)‖ ≤ e n) :72 ∃ g : Space D, evalZero D g = M (evalZero D f) ∧ |‖g‖ - ‖f‖| ≤ ∑' n, e n := by73 let g := ofSummable D h0 (M (evalZero D f))74 (summable_product_coordinates M f e he hpres hcomm)75 have hg : evalZero D g = M (evalZero D f) := evalZero_ofSummable D h0 _ _76 exact ⟨g, hg, norm_product_sub_norm_le M f g hg e he hpres hcomm⟩7778/-- Coordinatewise separation survives the summable commutator error. -/79theorem separation (M : Y →L[𝕜] Y) (h f g : Space D)80 (hg : evalZero D g = M (evalZero D f)) (e : ℕ → ℝ) (he : Summable e)81 (c : ℝ)82 (hsep : ∀ n, c * (‖coord D n h‖ + ‖coord D n f‖) ≤83 ‖coord D n h + M (coord D n f)‖)84 (hcomm : ∀ n, ‖D n (M (evalZero D f)) - M (coord D n f)‖ ≤ e n) :85 c * (‖h‖ + ‖f‖) - (∑' n, e n) ≤ ‖h + g‖ := by86 have hbound (n : ℕ) : c * (‖coord D n h‖ + ‖coord D n f‖) ≤87 ‖coord D n (h + g)‖ + e n := by88 have heq : coord D n h + M (coord D n f) =89 coord D n (h + g) - (coord D n g - M (coord D n f)) := by90 rw [map_add]91 abel92 have herr : ‖coord D n g - M (coord D n f)‖ ≤ e n := by93 rw [coord_eq, hg]94 exact hcomm n95 calc96 _ ≤ ‖coord D n h + M (coord D n f)‖ := hsep n97 _ = ‖coord D n (h + g) - (coord D n g - M (coord D n f))‖ := by rw [heq]98 _ ≤ ‖coord D n (h + g)‖ + ‖coord D n g - M (coord D n f)‖ := norm_sub_le _ _99 _ ≤ _ := add_le_add le_rfl herr100 have hs := (((summable_norm_coord h).add (summable_norm_coord f)).mul_left c).tsum_le_tsum101 hbound ((summable_norm_coord (h + g)).add he)102 rw [tsum_mul_left, (summable_norm_coord h).tsum_add (summable_norm_coord f),103 (summable_norm_coord (h + g)).tsum_add he, ← norm_eq_tsum, ← norm_eq_tsum,104 ← norm_eq_tsum] at hs105 linarith106107end PL1.IntrinsicSpikeEstimates108