PL1/SpikeSeparation.lean
All source files · Download exact source
SHA-256: beaa0764a6e4ff4c9f776536c80e35b4f72385189bad379abd20025ca36ae9c2
1import Mathlib.MeasureTheory.Integral.Bochner.Set2import Mathlib.MeasureTheory.Integral.Prod3import Mathlib.Analysis.RCLike.Basic4import Mathlib.Tactic.Linarith5import Mathlib.Tactic.Ring67/-! # Separation by a nonnegative concentrated density89These estimates use actual measurable sets and Bochner integrals. They apply10to arbitrary probability measures and, in fact, to vectors in any real11normed space. The scalar specialization includes real and complex fields.12-/1314noncomputable section15open MeasureTheory1617namespace PL1.SpikeSeparation1819variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]20variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]21variable {q : Ω → ℝ}2223theorem integrable_add_smul (hq : Integrable q μ) (b c : E) :24 Integrable (fun x => b + q x • c) μ := (integrable_const b).add (hq.smul_const c)2526theorem integrable_norm_add_smul (hq : Integrable q μ) (b c : E) :27 Integrable (fun x => ‖b + q x • c‖) μ := (integrable_add_smul hq b c).norm2829private theorem pointwise_left (b c : E) (t : ℝ) (ht : 0 ≤ t) :30 t * ‖c‖ - ‖b‖ ≤ ‖b + t • c‖ := by31 simpa only [norm_neg, sub_neg_eq_add, norm_smul, Real.norm_eq_abs, abs_of_nonneg ht,32 add_comm] using norm_sub_norm_le (t • c) (-b)3334private theorem pointwise_right (b c : E) (t : ℝ) (ht : 0 ≤ t) :35 ‖b‖ - t * ‖c‖ ≤ ‖b + t • c‖ := by36 simpa only [norm_neg, sub_neg_eq_add, norm_smul, Real.norm_eq_abs, abs_of_nonneg ht]37 using norm_sub_norm_le b (-(t • c))3839/-- The two reverse-triangle bounds integrated over a set and its complement. -/40theorem split_estimates (hq : Integrable q μ) (hq0 : ∀ᵐ x ∂μ, 0 ≤ q x)41 (B : Set Ω) (b c : E) :42 (∫ x in B, q x ∂μ) * ‖c‖ - μ.real B * ‖b‖ ≤ ∫ x in B, ‖b + q x • c‖ ∂μ ∧43 μ.real Bᶜ * ‖b‖ - (∫ x in Bᶜ, q x ∂μ) * ‖c‖ ≤44 ∫ x in Bᶜ, ‖b + q x • c‖ ∂μ := by45 have hn := integrable_norm_add_smul hq b c46 constructor47 · have h := integral_mono_ae ((hq.mul_const ‖c‖).sub (integrable_const ‖b‖)).integrableOn48 hn.integrableOn (show ∀ᵐ x ∂μ.restrict B, q x * ‖c‖ - ‖b‖ ≤ ‖b + q x • c‖ from by49 filter_upwards [ae_restrict_of_ae hq0] with x hx50 exact pointwise_left b c (q x) hx)51 simpa only [Pi.sub_apply, integral_sub (hq.integrableOn.mul_const ‖c‖) (integrable_const ‖b‖),52 integral_mul_const, integral_const, smul_eq_mul, measureReal_def, Measure.restrict_apply_univ] using h53 · have h := integral_mono_ae ((integrable_const ‖b‖).sub (hq.mul_const ‖c‖)).integrableOn54 hn.integrableOn (show ∀ᵐ x ∂μ.restrict Bᶜ, ‖b‖ - q x * ‖c‖ ≤ ‖b + q x • c‖ from by55 filter_upwards [ae_restrict_of_ae hq0] with x hx56 exact pointwise_right b c (q x) hx)57 simpa only [Pi.sub_apply, integral_sub (integrable_const ‖b‖) (hq.integrableOn.mul_const ‖c‖),58 integral_mul_const, integral_const, smul_eq_mul, measureReal_def, Measure.restrict_apply_univ] using h5960/-- Exact separation bound obtained by splitting over the concentration set. -/61theorem split_lower_bound (hq : Integrable q μ) (hq0 : ∀ᵐ x ∂μ, 0 ≤ q x)62 (hq1 : ∫ x, q x ∂μ = 1) (B : Set Ω) (hB : MeasurableSet B) (b c : E) :63 (1 - 2 * μ.real B) * ‖b‖ + (2 * (∫ x in B, q x ∂μ) - 1) * ‖c‖ ≤64 ∫ x, ‖b + q x • c‖ ∂μ := by65 obtain ⟨hleft, hright⟩ := split_estimates hq hq0 B b c66 have hmass := integral_add_compl hB hq67 have hmeasure : μ.real B + μ.real Bᶜ = 1 := by68 simpa using measureReal_add_measureReal_compl (μ := μ) hB69 have hnorm := integral_add_compl hB (integrable_norm_add_smul hq b c)70 rw [hq1] at hmass71 have hm := congrArg (fun t : ℝ => t * ‖c‖) hmass72 have hμ := congrArg (fun t : ℝ => t * ‖b‖) hmeasure73 nlinarith7475/-- A unit-mass nonnegative density concentrated on a small set separates all vectors. -/76theorem concentration_lower_bound (hq : Integrable q μ) (hq0 : ∀ᵐ x ∂μ, 0 ≤ q x)77 (hq1 : ∫ x, q x ∂μ = 1) (B : Set Ω) (hB : MeasurableSet B) (δ : ℝ)78 (hsmall : μ.real B ≤ δ) (hconcentrated : 1 - δ ≤ ∫ x in B, q x ∂μ) (b c : E) :79 (1 - 2 * δ) * (‖b‖ + ‖c‖) ≤ ∫ x, ‖b + q x • c‖ ∂μ := by80 have hs := split_lower_bound hq hq0 hq1 B hB b c81 have hb := mul_le_mul_of_nonneg_right (show 1 - 2 * δ ≤ 1 - 2 * μ.real B by linarith)82 (norm_nonneg b)83 have hc := mul_le_mul_of_nonneg_right84 (show 1 - 2 * δ ≤ 2 * (∫ x in B, q x ∂μ) - 1 by linarith) (norm_nonneg c)85 nlinarith8687variable {𝕜 : Type*} [RCLike 𝕜]8889theorem integrable_norm_add_mul (hq : Integrable q μ) (b c : 𝕜) :90 Integrable (fun x => ‖b + c * (q x : 𝕜)‖) μ := by91 simpa only [Algebra.smul_def, RCLike.algebraMap_eq_ofReal, mul_comm] using92 integrable_norm_add_smul hq b c9394/-- The exact scalar inequality used in the manuscript, over both scalar fields. -/95theorem concentration_lower_bound_rclike (hq : Integrable q μ) (hq0 : ∀ᵐ x ∂μ, 0 ≤ q x)96 (hq1 : ∫ x, q x ∂μ = 1) (B : Set Ω) (hB : MeasurableSet B) (δ : ℝ)97 (hsmall : μ.real B ≤ δ) (hconcentrated : 1 - δ ≤ ∫ x in B, q x ∂μ) (b c : 𝕜) :98 (1 - 2 * δ) * (‖b‖ + ‖c‖) ≤ ∫ x, ‖b + c * (q x : 𝕜)‖ ∂μ := by99 simpa only [Algebra.smul_def, RCLike.algebraMap_eq_ofReal, mul_comm] using100 concentration_lower_bound hq hq0 hq1 B hB δ hsmall hconcentrated b c101102section Product103104variable {H : Type*} [MeasurableSpace H] {ν : Measure H} [SFinite ν]105variable {b c : H → E}106107theorem integrable_prod_add_smul (hb : Integrable b ν) (hc : Integrable c ν)108 (hq : Integrable q μ) :109 Integrable (fun z : H × Ω => b z.1 + q z.2 • c z.1) (ν.prod μ) := by110 exact (hb.comp_fst μ).add ((hq.smul_prod hc).swap)111112/-- Integrating the scalar/vector separation inequality over independent head coordinates. -/113theorem product_concentration_lower_bound (hb : Integrable b ν) (hc : Integrable c ν)114 (hq : Integrable q μ) (hq0 : ∀ᵐ x ∂μ, 0 ≤ q x) (hq1 : ∫ x, q x ∂μ = 1)115 (B : Set Ω) (hB : MeasurableSet B) (δ : ℝ)116 (hsmall : μ.real B ≤ δ) (hconcentrated : 1 - δ ≤ ∫ x in B, q x ∂μ) :117 (1 - 2 * δ) * ((∫ y, ‖b y‖ ∂ν) + ∫ y, ‖c y‖ ∂ν) ≤118 ∫ z : H × Ω, ‖b z.1 + q z.2 • c z.1‖ ∂(ν.prod μ) := by119 have hint := (integrable_prod_add_smul hb hc hq).norm120 rw [integral_prod _ hint]121 have h := integral_mono_ae ((hb.norm.add hc.norm).const_mul (1 - 2 * δ))122 hint.integral_prod_left (Filter.Eventually.of_forall (fun y =>123 concentration_lower_bound hq hq0 hq1 B hB δ hsmall hconcentrated (b y) (c y)))124 simpa only [Pi.add_apply, integral_const_mul, integral_add hb.norm hc.norm] using h125126end Product127128#print axioms split_lower_bound129#print axioms concentration_lower_bound_rclike130#print axioms product_concentration_lower_bound131132end PL1.SpikeSeparation133