PL1/MainInterpolation.lean
All source files · Download exact source
SHA-256: 81d2965528aa6958932f54da39d7c6747bdbea3143ebcffe49af6db2e69565e7
1import PL1.KFunctionalIntegral2import PL1.GeneratorGraphBanach34/-!5# The full interpolation identification with the actual generator domain67The norm below is the standard real interpolation integral at (1/2, 1),8defined directly from the actual complete graph-norm domain of the positive9generator. Its finite functions are exactly the original intrinsic space.10All statements hold for every nonnegative coordinate rate sequence, hence11for both manuscript constructions over either scalar field.12-/1314noncomputable section15open MeasureTheory16open scoped ENNReal NNReal1718namespace PL1.Interpolation19open Noise Walsh IntrinsicGraph ResolventEstimates2021variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)2223/-- The extended standard (Y,D(A))_{1/2,1} norm, with D(A)'s actual sum norm. -/24def normIntegral (f : Lp K 1 haar) : ℝ≥0∞ :=25 ∫⁻ t in Set.Ioi (0 : ℝ), ENNReal.ofReal (t ^ (-3 / 2 : ℝ) *26 sInf (Set.range (fun z : GeneratorGraphBanach.Domain K rates =>27 ‖f - GeneratorGraphBanach.inclusion K rates z‖ + t * ‖z‖)))2829theorem normIntegral_eq (f : Lp K 1 haar) :30 normIntegral K rates f = KFunctional.continuousNorm K rates f := by31 unfold normIntegral KFunctional.continuousNorm32 congr 133 funext t34 rw [GeneratorGraphBanach.kFunctional_eq]3536/-- Equality as spaces of actual Haar-L1 functions. -/37theorem mem_intrinsic_iff (f : Lp K 1 haar) :38 f ∈ (evalZero (dyadicSystem K rates).analysis).range ↔ normIntegral K rates f < ⊤ := by39 rw [normIntegral_eq, lt_top_iff_ne_top, KFunctional.continuousNorm_ne_top_iff,40 DiscreteInterpolation.extendedNorm_ne_top_iff]4142theorem normIntegral_eval_ne_top (x : (dyadicSystem K rates).IntrinsicSpace) :43 normIntegral K rates (evalZero (dyadicSystem K rates).analysis x) ≠ ⊤ :=44 ((mem_intrinsic_iff K rates _).mp ⟨x, rfl⟩).ne4546/-- The real value is used only on the finite domain in the norm comparisons. -/47def normValue (f : Lp K 1 haar) : ℝ := (normIntegral K rates f).toReal4849theorem normValue_lower (x : (dyadicSystem K rates).IntrinsicSpace) :50 (1 / 10 : ℝ) * ‖x‖ ≤ normValue K rates (evalZero (dyadicSystem K rates).analysis x) := by51 let f := evalZero (dyadicSystem K rates).analysis x52 have hI : KFunctional.continuousNorm K rates f ≠ ⊤ := by53 rw [← normIntegral_eq]54 exact normIntegral_eval_ne_top K rates x55 have h := ENNReal.toReal_mono (ENNReal.mul_ne_top (by norm_num : (5 : ℝ≥0∞) ≠ ⊤) hI)56 (KFunctional.extendedNorm_le_five_continuousNorm K rates f)57 rw [DiscreteInterpolation.extendedNorm_eval_eq] at h58 have hd : 0 ≤ DiscreteInterpolation.normValue K rates f :=59 add_nonneg (norm_nonneg _) (tsum_nonneg (DiscreteInterpolation.term_nonneg K rates f))60 rw [ENNReal.toReal_ofReal hd, ENNReal.toReal_mul] at h61 norm_num only [ENNReal.toReal_ofNat] at h62 have hl := DiscreteInterpolation.half_norm_le K rates x63 change (1 / 2 : ℝ) * ‖x‖ ≤ DiscreteInterpolation.normValue K rates f at hl64 rw [normValue, normIntegral_eq]65 change (1 / 10 : ℝ) * ‖x‖ ≤ (KFunctional.continuousNorm K rates f).toReal66 linarith6768theorem normValue_upper (x : (dyadicSystem K rates).IntrinsicSpace) :69 normValue K rates (evalZero (dyadicSystem K rates).analysis x) ≤70 (4 * (2 + dyadicRatio / (1 - dyadicRatio))) * ‖x‖ := by71 let f := evalZero (dyadicSystem K rates).analysis x72 have hD : DiscreteInterpolation.extendedNorm K rates f ≠ ⊤ :=73 (DiscreteInterpolation.extendedNorm_ne_top_iff K rates f).mpr ⟨x, rfl⟩74 have h := ENNReal.toReal_mono (ENNReal.mul_ne_top (by norm_num : (4 : ℝ≥0∞) ≠ ⊤) hD)75 (KFunctional.continuousNorm_le_four_extendedNorm K rates f)76 rw [DiscreteInterpolation.extendedNorm_eval_eq] at h77 have hd : 0 ≤ DiscreteInterpolation.normValue K rates f :=78 add_nonneg (norm_nonneg _) (tsum_nonneg (DiscreteInterpolation.term_nonneg K rates f))79 rw [ENNReal.toReal_mul, ENNReal.toReal_ofReal hd] at h80 norm_num only [ENNReal.toReal_ofNat] at h81 have hu := DiscreteInterpolation.normValue_le K rates x82 change DiscreteInterpolation.normValue K rates f ≤83 (2 + dyadicRatio / (1 - dyadicRatio)) * ‖x‖ at hu84 rw [normValue, normIntegral_eq]85 change (KFunctional.continuousNorm K rates f).toReal ≤ _86 nlinarith8788/-- Full function-space identification and universal equivalent-norm bounds. -/89theorem intrinsic_eq_realInterpolation :90 (∀ f : Lp K 1 haar,91 f ∈ (evalZero (dyadicSystem K rates).analysis).range ↔ normIntegral K rates f < ⊤) ∧92 ∃ c C : ℝ, 0 < c ∧ 0 < C ∧93 ∀ x : (dyadicSystem K rates).IntrinsicSpace,94 c * ‖x‖ ≤ normValue K rates (evalZero (dyadicSystem K rates).analysis x) ∧95 normValue K rates (evalZero (dyadicSystem K rates).analysis x) ≤ C * ‖x‖ := by96 refine ⟨mem_intrinsic_iff K rates, 1 / 10,97 4 * (2 + dyadicRatio / (1 - dyadicRatio)), by norm_num, ?_, ?_⟩98 · have hc : 0 ≤ dyadicRatio / (1 - dyadicRatio) :=99 div_nonneg dyadicRatio_nonneg one_sub_dyadicRatio_pos.le100 positivity101 · exact fun x => ⟨normValue_lower K rates x, normValue_upper K rates x⟩102103theorem schur_mem_intrinsic_iff (f : Lp K 1 haar) :104 f ∈ (evalZero (dyadicSystem K schurRates).analysis).range ↔ normIntegral K schurRates f < ⊤ :=105 mem_intrinsic_iff K schurRates f106107theorem constant_mem_intrinsic_iff (f : Lp K 1 haar) :108 f ∈ (evalZero (dyadicSystem K constantRates).analysis).range ↔ normIntegral K constantRates f < ⊤ :=109 mem_intrinsic_iff K constantRates f110111end PL1.Interpolation112