PL1/KFunctionalProperties.lean
All source files · Download exact source
SHA-256: 2fa4ce33a1eb987fafdb0c66b696e6c60365795d02436a26de3e96186b8f3426
1import PL1.GeneratorGraphBanach23/-! # Standard norm properties of the actual graph K-functional -/45noncomputable section6open MeasureTheory7open scoped ENNReal NNReal89namespace PL1.KFunctional10open Noise Walsh ResolventGeneratorGraph1112variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)1314@[simp] theorem value_zero {t : ℝ} (ht : 0 ≤ t) : value K rates t 0 = 0 := by15 apply le_antisymm16 · simpa only [norm_zero] using value_le_norm K rates ht 017 · exact value_nonneg K rates ht 01819theorem min_mul_norm_le {t : ℝ} (ht : 0 ≤ t) (f : Lp K 1 haar) :20 min 1 t * ‖f‖ ≤ value K rates t f := by21 apply le_value K rates22 intro z23 have hc : 0 ≤ min 1 t := le_min zero_le_one ht24 have htriangle := mul_le_mul_of_nonneg_left (norm_le_norm_sub_add f z.val.1) hc25 have hfirst := mul_le_mul_of_nonneg_right (min_le_left 1 t) (norm_nonneg (f-z.val.1))26 have hsecond := mul_le_mul_of_nonneg_right (min_le_right 1 t) (norm_nonneg z.val.1)27 have hlast := mul_nonneg ht (norm_nonneg z.val.2)28 dsimp only [cost, graphNorm]29 nlinarith3031theorem cost_le_norm_sub_add_cost {t : ℝ} (f g : Lp K 1 haar) (z : graph K rates) :32 cost K rates t f z ≤ ‖f-g‖ + cost K rates t g z := by33 have h : f-z.val.1 = (f-g)+(g-z.val.1) := by abel34 have htri := norm_add_le (f-g) (g-z.val.1)35 rw [← h] at htri36 dsimp only [cost]37 linarith3839theorem value_le_norm_sub_add_value {t : ℝ} (ht : 0 ≤ t) (f g : Lp K 1 haar) :40 value K rates t f ≤ ‖f-g‖ + value K rates t g := by41 have h : value K rates t f - ‖f-g‖ ≤ value K rates t g := by42 apply le_value K rates43 intro z44 have h1 := value_le_cost K rates ht f z45 have h2 := cost_le_norm_sub_add_cost K rates f g z (t:=t)46 linarith47 linarith4849theorem abs_value_sub_le {t : ℝ} (ht : 0 ≤ t) (f g : Lp K 1 haar) :50 |value K rates t f - value K rates t g| ≤ ‖f-g‖ := by51 apply abs_le.mpr52 have hfg := value_le_norm_sub_add_value K rates ht f g53 have hgf := value_le_norm_sub_add_value K rates ht g f54 rw [norm_sub_rev g f] at hgf55 constructor <;> linarith5657theorem lipschitzWith_value {t : ℝ} (ht : 0 ≤ t) :58 LipschitzWith 1 (value K rates t) := by59 apply LipschitzWith.of_dist_le_mul60 intro f g61 simpa only [NNReal.coe_one, one_mul, Real.dist_eq, dist_eq_norm, Real.norm_eq_abs] using62 abs_value_sub_le K rates ht f g6364theorem continuous_value {t : ℝ} (ht : 0 ≤ t) : Continuous (value K rates t) :=65 (lipschitzWith_value K rates ht).continuous6667theorem cost_add_le {t : ℝ} (ht : 0 ≤ t) (f g : Lp K 1 haar)68 (z w : graph K rates) :69 cost K rates t (f+g) (z+w) ≤ cost K rates t f z + cost K rates t g w := by70 have he : f+g-(z.val.1+w.val.1) = (f-z.val.1)+(g-w.val.1) := by abel71 have h1 := norm_add_le (f-z.val.1) (g-w.val.1)72 have h2 := mul_le_mul_of_nonneg_left (norm_add_le z.val.1 w.val.1) ht73 have h3 := mul_le_mul_of_nonneg_left (norm_add_le z.val.2 w.val.2) ht74 change ‖f+g-(z.val.1+w.val.1)‖+t*(‖z.val.1+w.val.1‖+‖z.val.2+w.val.2‖) ≤ _75 rw [he]76 dsimp only [cost, graphNorm]77 nlinarith7879theorem value_add_le {t : ℝ} (ht : 0 ≤ t) (f g : Lp K 1 haar) :80 value K rates t (f+g) ≤ value K rates t f + value K rates t g := by81 have h : value K rates t (f+g)-value K rates t g ≤ value K rates t f := by82 apply le_value K rates83 intro z84 have hz : value K rates t (f+g)-cost K rates t f z ≤ value K rates t g := by85 apply le_value K rates86 intro w87 have h1 := value_le_cost K rates ht (f+g) (z+w)88 have h2 := cost_add_le K rates ht f g z w89 linarith90 linarith91 linarith9293theorem cost_smul {t : ℝ} (a : K) (f : Lp K 1 haar) (z : graph K rates) :94 cost K rates t (a • f) (a • z) = ‖a‖ * cost K rates t f z := by95 change ‖a • f - a • z.val.1‖ + t * (‖a • z.val.1‖ + ‖a • z.val.2‖) = _96 rw [← smul_sub]97 simp only [norm_smul, cost, graphNorm]98 ring99100theorem value_smul_le {t : ℝ} (ht : 0 ≤ t) (a : K) (f : Lp K 1 haar) :101 value K rates t (a • f) ≤ ‖a‖ * value K rates t f := by102 by_cases ha : a=0103 · simp only [ha, zero_smul, norm_zero, zero_mul, value_zero K rates ht]104 exact le_rfl105 have hnorm : 0 < ‖a‖ := norm_pos_iff.mpr ha106 rw [mul_comm ‖a‖]107 apply (div_le_iff₀ hnorm).mp108 apply le_value K rates109 intro z110 apply (div_le_iff₀ hnorm).mpr111 simpa only [cost_smul, mul_comm] using value_le_cost K rates ht (a • f) (a • z)112113theorem value_smul {t : ℝ} (ht : 0 ≤ t) (a : K) (f : Lp K 1 haar) :114 value K rates t (a • f) = ‖a‖ * value K rates t f := by115 apply le_antisymm (value_smul_le K rates ht a f)116 by_cases ha : a=0117 · simp only [ha, zero_smul, norm_zero, zero_mul, value_zero K rates ht]118 exact le_rfl119 have h := mul_le_mul_of_nonneg_left120 (value_smul_le K rates ht a⁻¹ (a • f)) (norm_nonneg a)121 simpa only [inv_smul_smul₀ ha, norm_inv, ← mul_assoc,122 mul_inv_cancel₀ (norm_ne_zero_iff.mpr ha), one_mul] using h123124end PL1.KFunctional125