PL1/KFunctional.lean
All source files · Download exact source
SHA-256: 2ea45edac5715b5e1cd8add454e668a93df2ee0aac6afcd23255f7ffa9267292
1import PL1.ResolventGeneratorGraph23/-!4# The actual graph K-functional and its resolvent bounds56The infimum ranges over the proved resolvent graph and uses the explicit sum7of its two L¹ norms. All estimates concern this actual infimum; monotonicity8is restricted to nonnegative time, the domain relevant to interpolation.9-/1011noncomputable section12open MeasureTheory13open scoped ENNReal NNReal1415namespace PL1.KFunctional16open Noise Walsh ResolventGeneratorGraph1718variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)1920def cost (t : ℝ) (f : Lp K 1 haar) (z : graph K rates) : ℝ :=21 ‖f - z.val.1‖ + t * graphNorm K z.val2223def value (t : ℝ) (f : Lp K 1 haar) : ℝ := sInf (Set.range (cost K rates t f))2425theorem cost_nonneg {t : ℝ} (ht : 0 ≤ t) (f : Lp K 1 haar) (z : graph K rates) :26 0 ≤ cost K rates t f z :=27 add_nonneg (norm_nonneg _) (mul_nonneg ht (graphNorm_nonneg K z.val))2829theorem cost_range_bddBelow {t : ℝ} (ht : 0 ≤ t) (f : Lp K 1 haar) :30 BddBelow (Set.range (cost K rates t f)) :=31 ⟨0, by rintro _ ⟨z, rfl⟩; exact cost_nonneg K rates ht f z⟩3233theorem le_value {t c : ℝ} (f : Lp K 1 haar)34 (hc : ∀ z : graph K rates, c ≤ cost K rates t f z) : c ≤ value K rates t f :=35 le_csInf (Set.range_nonempty _) (by rintro _ ⟨z, rfl⟩; exact hc z)3637theorem value_nonneg {t : ℝ} (ht : 0 ≤ t) (f : Lp K 1 haar) :38 0 ≤ value K rates t f := le_value K rates f (cost_nonneg K rates ht f)3940theorem value_le_cost {t : ℝ} (ht : 0 ≤ t) (f : Lp K 1 haar) (z : graph K rates) :41 value K rates t f ≤ cost K rates t f z :=42 csInf_le (cost_range_bddBelow K rates ht f) ⟨z, rfl⟩4344theorem value_le_norm {t : ℝ} (ht : 0 ≤ t) (f : Lp K 1 haar) :45 value K rates t f ≤ ‖f‖ := by46 simpa only [cost, graphNorm, ZeroMemClass.coe_zero, Prod.fst_zero, Prod.snd_zero,47 sub_zero, norm_zero, add_zero, mul_zero] using value_le_cost K rates ht f 04849theorem value_eq_norm_of_one_le {t : ℝ} (ht : 1 ≤ t) (f : Lp K 1 haar) :50 value K rates t f = ‖f‖ := by51 apply le_antisymm (value_le_norm K rates (zero_le_one.trans ht) f)52 apply le_value K rates53 intro z54 have hnorm := norm_le_norm_sub_add f z.val.155 have hgraph : ‖z.val.1‖ ≤ graphNorm K z.val :=56 le_add_of_nonneg_right (norm_nonneg _)57 have hmul := mul_le_mul_of_nonneg_right ht (graphNorm_nonneg K z.val)58 dsimp only [cost]59 linarith6061theorem value_mono {s t : ℝ} (hs : 0 ≤ s) (hst : s ≤ t) (f : Lp K 1 haar) :62 value K rates s f ≤ value K rates t f := by63 apply le_value K rates64 intro z65 apply (value_le_cost K rates hs f z).trans66 exact add_le_add le_rfl (mul_le_mul_of_nonneg_right hst (graphNorm_nonneg K z.val))6768theorem monotoneOn_value (f : Lp K 1 haar) :69 MonotoneOn (fun t => value K rates t f) (Set.Ici (0 : ℝ)) :=70 fun _ hs _ _ hst => value_mono K rates hs hst f7172theorem value_div_antitone {s t : ℝ} (hs : 0 < s) (hst : s ≤ t) (f : Lp K 1 haar) :73 value K rates t f / t ≤ value K rates s f / s := by74 have ht : 0 < t := hs.trans_le hst75 apply (le_div_iff₀ hs).mpr76 apply le_value K rates77 intro z78 have hcost := div_le_div_of_nonneg_right (value_le_cost K rates ht.le f z) ht.le79 apply (mul_le_mul_of_nonneg_right hcost hs.le).trans80 rw [div_mul_eq_mul_div]81 apply (div_le_iff₀ ht).mpr82 have h := mul_le_mul_of_nonneg_left hst (norm_nonneg (f - z.val.1))83 dsimp only [cost]84 nlinarith8586theorem antitoneOn_value_div (f : Lp K 1 haar) :87 AntitoneOn (fun t => value K rates t f / t) (Set.Ioi (0 : ℝ)) :=88 fun _ hs _ _ hst => value_div_antitone K rates hs hst f8990theorem norm_defect_le_two_cost (t : PositiveTime) (f : Lp K 1 haar) (z : graph K rates) :91 ‖f - resolventL1 K rates t f‖ ≤ 2 * cost K rates t f z := by92 have heq : f - resolventL1 K rates t f =93 ((f - z.val.1) - resolventL1 K rates t (f - z.val.1)) +94 (z.val.1 - resolventL1 K rates t z.val.1) := by rw [map_sub]; abel95 have htri := norm_add_le96 ((f - z.val.1) - resolventL1 K rates t (f - z.val.1))97 (z.val.1 - resolventL1 K rates t z.val.1)98 rw [← heq] at htri99 have hdiff := norm_sub_le (f - z.val.1) (resolventL1 K rates t (f - z.val.1))100 have hc := norm_resolvent_apply_le K rates t (f - z.val.1)101 have hg := norm_defect_le K rates t z.property102 have hnon1 := mul_nonneg t.property.le (norm_nonneg z.val.1)103 have hnon2 := mul_nonneg t.property.le (norm_nonneg z.val.2)104 dsimp only [cost, graphNorm]105 nlinarith106107theorem half_norm_defect_le (t : PositiveTime) (f : Lp K 1 haar) :108 (1 / 2 : ℝ) * ‖f - resolventL1 K rates t f‖ ≤ value K rates t f := by109 apply le_value K rates110 intro z111 linarith [norm_defect_le_two_cost K rates t f z]112113theorem value_le_defect (t : PositiveTime) (f : Lp K 1 haar) :114 value K rates t f ≤ 2 * ‖f - resolventL1 K rates t f‖ + (t : ℝ) * ‖f‖ := by115 let z : graph K rates := ⟨(resolventL1 K rates t f,116 (((t : ℝ)⁻¹ : ℝ) : K) • (f - resolventL1 K rates t f)), resolvent_pair_mem K rates t f⟩117 apply (value_le_cost K rates t.property.le f z).trans118 have hc := mul_le_mul_of_nonneg_left (norm_resolvent_apply_le K rates t f) t.property.le119 have he : (t : ℝ) * ((t : ℝ)⁻¹ * ‖f - resolventL1 K rates t f‖) =120 ‖f - resolventL1 K rates t f‖ := by rw [← mul_assoc, mul_inv_cancel₀ t.property.ne', one_mul]121 simp only [cost, z, graphNorm, norm_smul, RCLike.norm_ofReal,122 abs_of_pos (inv_pos.mpr t.property)]123 nlinarith124125end PL1.KFunctional126