PL1/InterpolationNorm.lean
All source files · Download exact source
SHA-256: 43b446d18533f339061f9b90b0327fc78014017112d84a55f7e983e4b4c602ed
1import PL1.MainInterpolation2import PL1.KFunctionalNormLaws3import Mathlib.Analysis.Normed.Module.Seminorm.Basic45/-!6# The actual real-interpolation integral as a complete Banach norm78`Space` is a dedicated type alias with the standard integral norm. The9original intrinsic norm and all its geometric theorems keep their original10instances. The identity is a continuous linear equivalence in both directions.11-/1213noncomputable section14open MeasureTheory15open scoped ENNReal NNReal1617namespace PL1.InterpolationNorm18open Noise Walsh IntrinsicGraph ResolventEstimates1920variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)2122/-- The finite, actual interpolation integral evaluated on an intrinsic vector. -/23def value (x : (dyadicSystem K rates).IntrinsicSpace) : ℝ :=24 Interpolation.normValue K rates (evalZero (dyadicSystem K rates).analysis x)2526theorem value_eq (x : (dyadicSystem K rates).IntrinsicSpace) :27 value K rates x =28 (KFunctional.continuousNorm K rates (evalZero (dyadicSystem K rates).analysis x)).toReal := by29 rw [value, Interpolation.normValue, Interpolation.normIntegral_eq]3031theorem continuousNorm_eval_ne_top (x : (dyadicSystem K rates).IntrinsicSpace) :32 KFunctional.continuousNorm K rates (evalZero (dyadicSystem K rates).analysis x) ≠ ⊤ := by33 rw [← Interpolation.normIntegral_eq]34 exact Interpolation.normIntegral_eval_ne_top K rates x3536theorem value_nonneg (x : (dyadicSystem K rates).IntrinsicSpace) : 0 ≤ value K rates x :=37 ENNReal.toReal_nonneg3839theorem value_zero : value K rates 0 = 0 := by40 rw [value_eq, map_zero, KFunctional.continuousNorm_zero, ENNReal.toReal_zero]4142theorem value_smul (a : K) (x : (dyadicSystem K rates).IntrinsicSpace) :43 value K rates (a • x) = ‖a‖ * value K rates x := by44 simp only [value_eq, map_smul, KFunctional.continuousNorm_smul,45 ENNReal.toReal_mul, ENNReal.toReal_ofReal (norm_nonneg a)]4647theorem value_add_le (x y : (dyadicSystem K rates).IntrinsicSpace) :48 value K rates (x+y) ≤ value K rates x + value K rates y := by49 have hx := continuousNorm_eval_ne_top K rates x50 have hy := continuousNorm_eval_ne_top K rates y51 have h := ENNReal.toReal_mono (ENNReal.add_ne_top.mpr ⟨hx, hy⟩)52 (KFunctional.continuousNorm_add_le K rates53 (evalZero (dyadicSystem K rates).analysis x) (evalZero (dyadicSystem K rates).analysis y))54 simpa only [value_eq, map_add, ENNReal.toReal_add hx hy] using h5556theorem value_lower (x : (dyadicSystem K rates).IntrinsicSpace) :57 (1/10 : ℝ) * ‖x‖ ≤ value K rates x := Interpolation.normValue_lower K rates x5859theorem value_upper (x : (dyadicSystem K rates).IntrinsicSpace) :60 value K rates x ≤ (4 * (2 + dyadicRatio / (1-dyadicRatio))) * ‖x‖ :=61 Interpolation.normValue_upper K rates x6263theorem eq_zero_of_value_eq_zero (x : (dyadicSystem K rates).IntrinsicSpace)64 (hx : value K rates x = 0) : x = 0 := by65 have h := value_lower K rates x66 apply norm_eq_zero.mp67 have hn := norm_nonneg x68 rw [hx] at h69 linarith7071/-- A separating seminorm on the original intrinsic space. -/72def seminorm : Seminorm K (dyadicSystem K rates).IntrinsicSpace :=73 Seminorm.of (value K rates) (value_add_le K rates) (value_smul K rates)7475/-- A dedicated copy carrying the standard interpolation integral norm. -/76def Space : Type _ := (dyadicSystem K rates).IntrinsicSpace7778instance : AddCommGroup (Space K rates) :=79 inferInstanceAs (AddCommGroup (dyadicSystem K rates).IntrinsicSpace)8081instance : Module K (Space K rates) :=82 inferInstanceAs (Module K (dyadicSystem K rates).IntrinsicSpace)8384/-- Identity on vectors, before supplying the new norm. -/85def linearEquiv : Space K rates ≃ₗ[K] (dyadicSystem K rates).IntrinsicSpace :=86 LinearEquiv.refl K (dyadicSystem K rates).IntrinsicSpace8788def groupNorm : AddGroupNorm (Space K rates) :=89 { (seminorm K rates).toAddGroupSeminorm with90 eq_zero_of_map_eq_zero' := eq_zero_of_value_eq_zero K rates }9192instance : NormedAddCommGroup (Space K rates) :=93 (groupNorm K rates).toNormedAddCommGroup9495theorem norm_eq (x : Space K rates) : ‖x‖ = value K rates (linearEquiv K rates x) := rfl9697instance : NormedSpace K (Space K rates) where98 norm_smul_le a x := by99 rw [norm_eq, norm_eq, map_smul]100 exact (value_smul K rates a (linearEquiv K rates x)).le101102/-- The original and standard integral norms give the same Banach topology. -/103def continuousLinearEquiv : Space K rates ≃L[K] (dyadicSystem K rates).IntrinsicSpace :=104 (linearEquiv K rates).toContinuousLinearEquivOfBounds105 10 (4 * (2 + dyadicRatio / (1-dyadicRatio)))106 (fun x => by107 rw [norm_eq]108 have h := value_lower K rates (linearEquiv K rates x)109 linarith)110 (fun x => by111 rw [norm_eq, LinearEquiv.apply_symm_apply]112 exact value_upper K rates x)113114instance : CompleteSpace (Space K rates) := by115 apply (completeSpace_iff_isComplete_range116 (continuousLinearEquiv K rates).isUniformEmbedding.isUniformInducing).mpr117 rw [(continuousLinearEquiv K rates).surjective.range_eq]118 exact isComplete_univ119120/-- Equality with the standard integral over the genuine generator-domain norm. -/121theorem norm_eq_integral (x : Space K rates) :122 ‖x‖ = (Interpolation.normIntegral K rates123 (evalZero (dyadicSystem K rates).analysis (continuousLinearEquiv K rates x))).toReal := rfl124125/-- The underlying Haar function is unchanged by the Banach-space identification. -/126def inclusion : Space K rates →L[K] Lp K 1 haar :=127 (evalZero (dyadicSystem K rates).analysis).comp128 (continuousLinearEquiv K rates).toContinuousLinearMap129130theorem inclusion_injective : Function.Injective (inclusion K rates) :=131 (evalZero_injective (dyadicSystem K rates).analysis).comp132 (continuousLinearEquiv K rates).injective133134end PL1.InterpolationNorm135