PL1/DiscreteInterpolation.lean
All source files · Download exact source
SHA-256: d9a54698353449cb31026e738d669148fe8196186c1fb2417c56288f20caac6f
1import PL1.KFunctional23/-!4# The discrete interpolation norm equals the intrinsic space56The K-functional is the actual infimum for the resolvent graph, using its7sum norm. Dyadic samples recover exactly the functions in the original8intrinsic graph, with explicit two-sided norm bounds.9-/1011noncomputable section12open MeasureTheory13open scoped ENNReal NNReal1415namespace PL1.DiscreteInterpolation16open Noise Walsh IntrinsicGraph ResolventEstimates1718variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)1920def term (f : Lp K 1 haar) (n : ℕ) : ℝ :=21 (dyadicRatio ^ (n + 1))⁻¹ * KFunctional.value K rates (dyadicTime (n + 1)) f2223/-- The discrete norm on summable inputs. Outside that domain, Lean's real24`tsum` convention does not represent an infinite interpolation norm; all25norm comparisons below are restricted to actual intrinsic vectors. -/26def normValue (f : Lp K 1 haar) : ℝ := ‖f‖ + ∑' n, term K rates f n2728theorem term_nonneg (f : Lp K 1 haar) (n : ℕ) : 0 ≤ term K rates f n :=29 mul_nonneg (inv_nonneg.mpr (pow_nonneg dyadicRatio_nonneg _))30 (KFunctional.value_nonneg K rates (dyadicTime (n + 1)).property.le f)3132theorem norm_analysis_succ (f : Lp K 1 haar) (n : ℕ) :33 ‖(dyadicSystem K rates).analysis (n + 1) f‖ =34 (dyadicRatio ^ (n + 1))⁻¹ * ‖f - resolventL1 K rates (dyadicTime (n + 1)) f‖ := by35 simp only [DyadicSystem.analysis, analysisCoordinate, smul_apply, sub_apply,36 ContinuousLinearMap.id_apply, norm_smul, RCLike.norm_ofReal,37 abs_of_nonneg (inv_nonneg.mpr (pow_nonneg dyadicRatio_nonneg _))]38 rfl3940theorem half_analysis_le_term (f : Lp K 1 haar) (n : ℕ) :41 (1 / 2 : ℝ) * ‖(dyadicSystem K rates).analysis (n + 1) f‖ ≤ term K rates f n := by42 have h := mul_le_mul_of_nonneg_left43 (KFunctional.half_norm_defect_le K rates (dyadicTime (n + 1)) f)44 (inv_nonneg.mpr (pow_nonneg dyadicRatio_nonneg (n + 1)))45 rw [norm_analysis_succ]46 dsimp only [term]47 nlinarith4849theorem term_le_analysis (f : Lp K 1 haar) (n : ℕ) :50 term K rates f n ≤ 2 * ‖(dyadicSystem K rates).analysis (n + 1) f‖ +51 dyadicRatio ^ (n + 1) * ‖f‖ := by52 have h := mul_le_mul_of_nonneg_left53 (KFunctional.value_le_defect K rates (dyadicTime (n + 1)) f)54 (inv_nonneg.mpr (pow_nonneg dyadicRatio_nonneg (n + 1)))55 rw [norm_analysis_succ]56 dsimp only [term]57 apply h.trans_eq58 simp only [dyadicTime, dyadicRatio_sq_pow]59 field_simp [dyadicRatio_pow_ne_zero]6061theorem summable_term_iff (f : Lp K 1 haar) :62 Summable (term K rates f) ↔63 Summable (fun n => ‖(dyadicSystem K rates).analysis n f‖) := by64 constructor65 · intro h66 apply (summable_nat_add_iff 1).mp67 apply Summable.of_nonneg_of_le (fun _ => norm_nonneg _) _ (h.mul_left 2)68 intro n69 linarith [half_analysis_le_term K rates f n]70 · intro h71 have h := (summable_nat_add_iff 1).mpr h72 apply Summable.of_nonneg_of_le (term_nonneg K rates f) (term_le_analysis K rates f)73 exact (h.mul_left 2).add (geometric_tail_summable.mul_right ‖f‖)7475theorem mem_range_evalZero_iff (f : Lp K 1 haar) :76 f ∈ (evalZero (dyadicSystem K rates).analysis).range ↔ Summable (term K rates f) := by77 rw [IntrinsicGraph.mem_range_evalZero_iff _ rfl, summable_term_iff]7879theorem summable_term_eval (x : (dyadicSystem K rates).IntrinsicSpace) :80 Summable (term K rates (evalZero (dyadicSystem K rates).analysis x)) :=81 (mem_range_evalZero_iff K rates _).mp ⟨x, rfl⟩8283theorem norm_eq_base_add_tail (x : (dyadicSystem K rates).IntrinsicSpace) :84 ‖x‖ = ‖evalZero (dyadicSystem K rates).analysis x‖ +85 ∑' n, ‖(dyadicSystem K rates).analysis (n + 1)86 (evalZero (dyadicSystem K rates).analysis x)‖ := by87 have h := (summable_term_iff K rates _).mp (summable_term_eval K rates x)88 rw [norm_eq_tsum_operators, h.tsum_eq_zero_add]89 rfl9091theorem half_norm_le (x : (dyadicSystem K rates).IntrinsicSpace) :92 (1 / 2 : ℝ) * ‖x‖ ≤ normValue K rates (evalZero (dyadicSystem K rates).analysis x) := by93 let f := evalZero (dyadicSystem K rates).analysis x94 have hb := summable_term_eval K rates x95 have ha := (summable_nat_add_iff 1).mpr ((summable_term_iff K rates f).mp hb)96 have hsum := (ha.mul_left (1 / 2 : ℝ)).tsum_le_tsum (half_analysis_le_term K rates f) hb97 rw [tsum_mul_left] at hsum98 rw [norm_eq_base_add_tail]99 dsimp only [normValue]100 have hf := norm_nonneg f101 change (1 / 2 : ℝ) * (‖f‖ + _) ≤ ‖f‖ + _102 linarith103104theorem normValue_le (x : (dyadicSystem K rates).IntrinsicSpace) :105 normValue K rates (evalZero (dyadicSystem K rates).analysis x) ≤106 (2 + dyadicRatio / (1 - dyadicRatio)) * ‖x‖ := by107 let f := evalZero (dyadicSystem K rates).analysis x108 have hb := summable_term_eval K rates x109 have ha := (summable_nat_add_iff 1).mpr ((summable_term_iff K rates f).mp hb)110 have he := geometric_tail_summable.mul_right ‖f‖111 have hsum := hb.tsum_le_tsum (term_le_analysis K rates f) ((ha.mul_left 2).add he)112 rw [Summable.tsum_add (ha.mul_left 2) he, tsum_mul_left, tsum_mul_right,113 geometric_tail_tsum] at hsum114 have ht : 0 ≤ ∑' n, ‖(dyadicSystem K rates).analysis (n + 1) f‖ := tsum_nonneg (fun _ => norm_nonneg _)115 have hc : 0 ≤ dyadicRatio / (1 - dyadicRatio) :=116 div_nonneg dyadicRatio_nonneg one_sub_dyadicRatio_pos.le117 have hct := mul_nonneg hc ht118 rw [norm_eq_base_add_tail]119 change ‖f‖ + _ ≤ (2 + dyadicRatio / (1 - dyadicRatio)) * (‖f‖ + _)120 nlinarith [norm_nonneg f]121122end PL1.DiscreteInterpolation123