PL1/ResolventMultiplication.lean

All source files · Download exact source

SHA-256: 73ea6be9be5637196cbfd3e08c9b06f64281e641d6a88965fa87121099fa69b9

1import PL1.BochnerResolvents2import PL1.L1Multiplication34/-! # Integrating actual semigroup commutator bounds -/56noncomputable section7open MeasureTheory8open scoped ENNReal NNReal910namespace PL1.Noise11open Walsh ExponentialTime1213variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)1415theorem resolvent_commutator_eq_integral (t : PositiveTime)16    (M : Lp K 1 haar →L[K] Lp K 1 haar) (f : Lp K 1 haar) :17    resolventL1 K rates t (M f) - M (resolventL1 K rates t f) =18      ∫ u, noiseL1 K rates u (M f) - M (noiseL1 K rates u f) ∂timeMeasure t := by19  let := isProbabilityMeasure_timeMeasure t.property20  rw [integral_sub (integrable_noiseL1 K rates _ (M f))21    (M.integrable_comp (integrable_noiseL1 K rates _ f)), M.integral_comp_comm22      (integrable_noiseL1 K rates _ f), ← resolventL1_eq_integral, ← resolventL1_eq_integral]2324theorem norm_resolvent_commutator_le (t T : PositiveTime)25    (M : Lp K 1 haar →L[K] Lp K 1 haar) (f : Lp K 1 haar)26    (hstep : ∀ u : ℝ≥0,27      ‖noiseL1 K rates u (M f) - M (noiseL1 K rates u f)‖ ≤28        2 * (1 - Real.exp (-(u : ℝ) / (T : ℝ))) * ‖f‖) :29    ‖resolventL1 K rates t (M f) - M (resolventL1 K rates t f)‖ ≤30      2 * (1 - (1 + (t : ℝ) * (T : ℝ)⁻¹)⁻¹) * ‖f‖ := by31  let := isProbabilityMeasure_timeMeasure t.property32  have hf := (integrable_noiseL1 K rates (timeMeasure t) (M f)).sub33    (M.integrable_comp (integrable_noiseL1 K rates (timeMeasure t) f))34  have hExp := integrable_laplace t.property (T : ℝ)⁻¹ (inv_nonneg.mpr T.property.le)35  have hb : Integrable (fun u : ℝ≥0 => 2 * (1 - Real.exp (-(u : ℝ) / (T : ℝ))) * ‖f‖)36      (timeMeasure t) := by37    simpa only [div_eq_mul_inv, Pi.sub_apply] using38      ((integrable_const (1 : ℝ)).sub hExp).const_mul 2 |>.mul_const ‖f‖39  rw [resolvent_commutator_eq_integral]40  apply (norm_integral_le_integral_norm _).trans41  apply (integral_mono hf.norm hb hstep).trans_eq42  rw [integral_mul_const, integral_const_mul]43  simp only [div_eq_mul_inv]44  rw [integral_sub (integrable_const 1) hExp, integral_laplace t.property _ (inv_nonneg.mpr T.property.le)]45  simp4647theorem norm_resolvent_commutator_le_time (t T : PositiveTime)48    (M : Lp K 1 haar →L[K] Lp K 1 haar) (f : Lp K 1 haar)49    (hstep : ∀ u : ℝ≥0,50      ‖noiseL1 K rates u (M f) - M (noiseL1 K rates u f)‖ ≤51        2 * (1 - Real.exp (-(u : ℝ) / (T : ℝ))) * ‖f‖) :52    ‖resolventL1 K rates t (M f) - M (resolventL1 K rates t f)‖ ≤53      (2 * (t : ℝ) / (T : ℝ)) * ‖f‖ := by54  apply (norm_resolvent_commutator_le K rates t T M f hstep).trans55  apply mul_le_mul_of_nonneg_right _ (norm_nonneg f)56  have hx : 0 ≤ (t : ℝ) * (T : ℝ)⁻¹ := mul_nonneg t.property.le (inv_nonneg.mpr T.property.le)57  have hden : 0 < 1 + (t : ℝ) * (T : ℝ)⁻¹ := by positivity58  have h : 1 - (1 + (t : ℝ) * (T : ℝ)⁻¹)⁻¹ ≤ (t : ℝ) * (T : ℝ)⁻¹ := by59    apply (le_of_mul_le_mul_right ?_ hden)60    nlinarith [mul_inv_cancel₀ hden.ne', sq_nonneg ((t : ℝ) * (T : ℝ)⁻¹)]61  simp only [div_eq_mul_inv]62  nlinarith6364theorem norm_id_sub_resolvent_commutator_le_time (t T : PositiveTime)65    (M : Lp K 1 haar →L[K] Lp K 1 haar) (f : Lp K 1 haar)66    (hstep : ∀ u : ℝ≥0,67      ‖noiseL1 K rates u (M f) - M (noiseL1 K rates u f)‖ ≤68        2 * (1 - Real.exp (-(u : ℝ) / (T : ℝ))) * ‖f‖) :69    ‖(M f - resolventL1 K rates t (M f)) - M (f - resolventL1 K rates t f)‖ ≤70      (2 * (t : ℝ) / (T : ℝ)) * ‖f‖ := by71  rw [map_sub]72  have heq : M f - resolventL1 K rates t (M f) - (M f - M (resolventL1 K rates t f)) =73      -(resolventL1 K rates t (M f) - M (resolventL1 K rates t f)) := by abel74  rw [heq, norm_neg]75  exact norm_resolvent_commutator_le_time K rates t T M f hstep7677end PL1.Noise78