PL1/ExtendedDiscreteInterpolation.lean

All source files · Download exact source

SHA-256: d3abb51ec3b9e1695af4a9aa4c6a162918d2cf02c889fb7653b45a4d6892a526

1import PL1.DiscreteInterpolation23/-! # Extended-valued discrete interpolation norm45The ENNReal quantity retains infinity on nonsummable inputs. Its finite6domain is exactly the original intrinsic space of functions.7-/89noncomputable section10open MeasureTheory11open scoped ENNReal NNReal1213namespace PL1.DiscreteInterpolation14open Noise Walsh IntrinsicGraph ResolventEstimates1516variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)1718def extendedNorm (f : Lp K 1 haar) : ℝ≥0∞ :=19  ENNReal.ofReal ‖f‖ + ∑' n, ENNReal.ofReal (term K rates f n)2021theorem tsum_term_ne_top_iff (f : Lp K 1 haar) :22    (∑' n, ENNReal.ofReal (term K rates f n)) ≠ ⊤ ↔ Summable (term K rates f) := by23  constructor24  · intro h25    have hs := ENNReal.summable_toReal h26    simpa only [ENNReal.toReal_ofReal (term_nonneg K rates f _)] using hs27  · exact Summable.tsum_ofReal_ne_top2829theorem extendedNorm_ne_top_iff (f : Lp K 1 haar) :30    extendedNorm K rates f ≠ ⊤ ↔ f ∈ (evalZero (dyadicSystem K rates).analysis).range := by31  rw [extendedNorm, ENNReal.add_ne_top, and_iff_right ENNReal.ofReal_ne_top,32    tsum_term_ne_top_iff, mem_range_evalZero_iff]3334theorem extendedNorm_eq_of_summable (f : Lp K 1 haar) (hf : Summable (term K rates f)) :35    extendedNorm K rates f = ENNReal.ofReal (normValue K rates f) := by36  rw [extendedNorm, normValue, ENNReal.ofReal_add (norm_nonneg _)37    (tsum_nonneg (term_nonneg K rates f)), ENNReal.ofReal_tsum_of_nonneg (term_nonneg K rates f) hf]3839theorem extendedNorm_eval_eq (x : (dyadicSystem K rates).IntrinsicSpace) :40    extendedNorm K rates (evalZero (dyadicSystem K rates).analysis x) =41      ENNReal.ofReal (normValue K rates (evalZero (dyadicSystem K rates).analysis x)) :=42  extendedNorm_eq_of_summable K rates _ (summable_term_eval K rates x)4344end PL1.DiscreteInterpolation45