PL1/ResolventNorms.lean

All source files · Download exact source

SHA-256: 23c680192d0f3fad1b93a0ffcce520cfd1ed083a6fd1457a22732398d35e0065

1import PL1.TruncatedResolventFactorization2import PL1.WalshBlocks34/-! # Exact norms of the actual resolvents and time cutoffs -/56noncomputable section7open MeasureTheory8open scoped ENNReal NNReal910namespace PL1.Noise11open Walsh WalshBlocks1213variable (𝕜 : Type*) [RCLike 𝕜] (rates : ℕ → ℝ≥0)1415theorem norm_resolventL1_eq_one (t : PositiveTime) : ‖resolventL1 𝕜 rates t‖ = 1 := by16  apply le_antisymm (norm_resolventL1_le_one 𝕜 rates t)17  have hf : scalarCharacterLp 𝕜 1 ∅ ≠ 0 := (linearIndependent_characterL1 𝕜).ne_zero ∅18  have hn := (resolventL1 𝕜 rates t).le_opNorm (scalarCharacterLp 𝕜 1 ∅)19  simp only [resolventL1_scalarCharacter, rateSum, Finset.sum_empty, mul_zero,20    add_zero, inv_one, RCLike.ofReal_one, one_smul] at hn21  nlinarith [norm_pos_iff.mpr hf]2223theorem norm_noiseL1_eq_one (u : ℝ≥0) : ‖noiseL1 𝕜 rates u‖ = 1 := by24  apply le_antisymm (norm_noiseL1_le_one 𝕜 rates u)25  have hf : scalarCharacterLp 𝕜 1 ∅ ≠ 0 := (linearIndependent_characterL1 𝕜).ne_zero ∅26  have hn := (noiseL1 𝕜 rates u).le_opNorm (scalarCharacterLp 𝕜 1 ∅)27  simp only [noiseL1_character, rateSum, Finset.sum_empty, mul_zero,28    Real.exp_zero, RCLike.ofReal_one, one_smul] at hn29  nlinarith [norm_pos_iff.mpr hf]3031theorem norm_truncatedResolventL1_eq (t : PositiveTime) (ε : ℝ≥0) :32    ‖truncatedResolventL1 𝕜 rates t ε‖ = Real.exp (-(ε : ℝ) / (t : ℝ)) := by33  apply le_antisymm34  · rw [truncatedResolventL1_eq_resolvent_comp_noise, norm_smul,35      RCLike.norm_ofReal, abs_of_pos (Real.exp_pos _)]36    have hb := ContinuousLinearMap.opNorm_comp_le37      (resolventL1 𝕜 rates t) (noiseL1 𝕜 rates ε)38    rw [norm_resolventL1_eq_one, norm_noiseL1_eq_one, mul_one] at hb39    simpa only [mul_one] using mul_le_mul_of_nonneg_left hb (Real.exp_pos _).le40  · have hf : scalarCharacterLp 𝕜 1 ∅ ≠ 0 := (linearIndependent_characterL1 𝕜).ne_zero ∅41    have he : truncatedResolventL1 𝕜 rates t ε (scalarCharacterLp 𝕜 1 ∅) =42        ((Real.exp (-(ε : ℝ) / (t : ℝ)) : ℝ) : 𝕜) • scalarCharacterLp 𝕜 1 ∅ := by43      rw [truncatedResolventL1_eq_resolvent_comp_noise]44      simp only [smul_apply, ContinuousLinearMap.comp_apply, noiseL1_character,45        resolventL1_scalarCharacter, rateSum, Finset.sum_empty, mul_zero,46        Real.exp_zero, add_zero, inv_one, RCLike.ofReal_one, one_smul]47    have hn := (truncatedResolventL1 𝕜 rates t ε).le_opNorm (scalarCharacterLp 𝕜 1 ∅)48    rw [he, norm_smul, RCLike.norm_ofReal, abs_of_pos (Real.exp_pos _)] at hn49    nlinarith [norm_pos_iff.mpr hf]5051theorem norm_resolventL1_sub_truncated_eq (t : PositiveTime) (ε : ℝ≥0) :52    ‖resolventL1 𝕜 rates t - truncatedResolventL1 𝕜 rates t ε‖ =53      1 - Real.exp (-(ε : ℝ) / (t : ℝ)) := by54  apply le_antisymm (norm_resolventL1_sub_truncated_le 𝕜 rates t ε)55  have hf : scalarCharacterLp 𝕜 1 ∅ ≠ 0 := (linearIndependent_characterL1 𝕜).ne_zero ∅56  have hnonneg : 0 ≤ 1 - Real.exp (-(ε : ℝ) / (t : ℝ)) := by57    apply sub_nonneg.mpr58    apply Real.exp_le_one_iff.mpr59    exact div_nonpos_of_nonpos_of_nonneg (neg_nonpos.mpr ε.coe_nonneg) t.property.le60  have he : (resolventL1 𝕜 rates t - truncatedResolventL1 𝕜 rates t ε)61      (scalarCharacterLp 𝕜 1 ∅) =62      (((1 - Real.exp (-(ε : ℝ) / (t : ℝ))) : ℝ) : 𝕜) • scalarCharacterLp 𝕜 1 ∅ := by63    rw [truncatedResolventL1_eq_resolvent_comp_noise]64    simp only [sub_apply, smul_apply, ContinuousLinearMap.comp_apply,65      noiseL1_character, resolventL1_scalarCharacter, rateSum,66      Finset.sum_empty, mul_zero, Real.exp_zero, add_zero, inv_one,67      RCLike.ofReal_one, one_smul, RCLike.ofReal_sub, sub_smul]68  have hn := (resolventL1 𝕜 rates t - truncatedResolventL1 𝕜 rates t ε).le_opNorm69    (scalarCharacterLp 𝕜 1 ∅)70  rw [he, norm_smul, RCLike.norm_ofReal, abs_of_nonneg hnonneg] at hn71  nlinarith [norm_pos_iff.mpr hf]7273end PL1.Noise74