PL1/IntrinsicTailNorm.lean
All source files · Download exact source
SHA-256: e0c0aa094ea1f4749a0a373725dec5bbb864f85aa0a3ce3ec94757f7cdce0f16
1import PL1.ConstantTailSpikes2import PL1.IntrinsicWalshBlocks3import PL1.L1Multiplication4import PL1.HeadTail5import PL1.IntrinsicSpikeFamilies67/-! # Exact tail expectations and norms in the original intrinsic space -/89noncomputable section10open MeasureTheory Filter11open scoped ENNReal NNReal Topology BigOperators1213namespace PL1.IntrinsicTailNorm14open Walsh WalshExpectations Noise IntrinsicGraph L1Multiplication1516variable (K : Type*) [RCLike K]1718theorem norm_constantL1 : ‖scalarCharacterLp K 1 ∅‖ = 1 := by19 rw [L1.norm_eq_integral_norm]20 have h : (fun x => ‖scalarCharacterLp K 1 ∅ x‖) =ᵐ[haar] fun _ => (1 : ℝ) := by21 filter_upwards [coeFn_scalarCharacterLp K 1 ∅] with x hx22 simp only [hx, scalarCharacter, character_empty, RCLike.ofReal_one, norm_one]23 rw [integral_congr_ae h]24 simp2526theorem coord_constant (rates : ℕ → ℝ≥0) (n : ℕ) :27 coord (dyadicSystem K rates).analysis n (intrinsicCharacter K rates ∅) =28 if n = 0 then scalarCharacterLp K 1 ∅ else 0 := by29 rw [coord_eq, evalZero_intrinsicCharacter]30 cases n with31 | zero => rfl32 | succ n =>33 change (((ResolventEstimates.dyadicRatio ^ (n + 1))⁻¹ : ℝ) : K) •34 (scalarCharacterLp K 1 ∅ - resolventL1 K rates (dyadicTime (n + 1))35 (scalarCharacterLp K 1 ∅)) = 036 rw [resolventL1_scalarCharacter]37 simp [rateSum]3839theorem norm_intrinsicConstant (rates : ℕ → ℝ≥0) :40 ‖intrinsicCharacter K rates ∅‖ = 1 := by41 rw [norm_eq_tsum]42 simp only [coord_constant, apply_ite norm, norm_zero]43 rw [tsum_ite_eq]44 exact norm_constantL1 K4546theorem intrinsicConstant_mem_range (rates : ℕ → ℝ≥0) (m : ℕ) :47 intrinsicCharacter K rates ∅ ∈ (intrinsicExpectation K rates m).range := by48 refine ⟨intrinsicCharacter K rates ∅, ?_⟩49 change intrinsicExpectation K rates m (intrinsicCharacter K rates ∅) = _50 simp only [intrinsicExpectation_character, Finset.empty_subset, ite_true]5152theorem multiplier_constant_ae (q : C(Walsh.Group, ℝ)) :53 multiplier K q (scalarCharacterLp K 1 ∅) =ᵐ[haar] fun x => (q x : K) := by54 filter_upwards [coeFn_multiplier K q (scalarCharacterLp K 1 ∅),55 coeFn_scalarCharacterLp K 1 ∅] with x hx hy56 rw [hx, hy]57 simp only [scalarCharacter, character_empty, RCLike.ofReal_one, RCLike.real_smul_eq_coe_mul, mul_one]5859/-- Averaging a finite tail density of integral one over the genuine tail60Haar subgroup gives the constant one, for every initial head length. -/61theorem expectation_multiplier_constant (m : ℕ) {S : Finset ℕ}62 (hS : Disjoint S (Finset.range m)) (q : C(Walsh.Group, ℝ))63 (hq : HeadTail.DependsOn S q) (hq1 : ∫ x, q x ∂haar = 1) :64 expectationL1 K m (multiplier K q (scalarCharacterLp K 1 ∅)) =65 scalarCharacterLp K 1 ∅ := by66 have hi (x : Walsh.Group) : (∫ y, (q (x * y) : K) ∂tailMeasure m) = 1 := by67 rw [tailMeasure, integral_map (continuous_tailProjection m).measurable.aemeasurable68 (RCLike.continuous_ofReal.comp69 (q.continuous.comp (continuous_const.mul continuous_id))).aestronglyMeasurable]70 have ht (y : Walsh.Group) : q (x * tailProjection m y) = q (x * y) := by71 apply hq72 intro j hj73 have hjm : ¬ j < m := by74 intro h75 exact Finset.disjoint_left.mp hS hj (Finset.mem_range.mpr h)76 simp only [Pi.mul_apply, tailProjection, hjm, ite_false]77 simp_rw [ht]78 rw [integral_mul_left_eq_self (fun y => (q y : K)) x]79 have he : (fun y => (q y : K)) = fun y => q y • (1 : K) := by80 funext y81 simp only [RCLike.real_smul_eq_coe_mul, mul_one]82 rw [he, integral_smul_const, hq1, one_smul]83 apply Lp.ext84 filter_upwards [convolutionL1_ae_eq_integral_of_ae_eq (tailMeasure m)85 (multiplier_constant_ae K q), coeFn_scalarCharacterLp K 1 ∅] with x hx hy86 change (convolutionL1 (tailMeasure m) (multiplier K q (scalarCharacterLp K 1 ∅))) x = _87 rw [hx, hi, hy]88 simp only [scalarCharacter, character_empty, RCLike.ofReal_one]8990theorem intrinsicExpectation_tailProduct (rates : ℕ → ℝ≥0) (m : ℕ)91 {S : Finset ℕ} (hS : Disjoint S (Finset.range m)) (q : C(Walsh.Group, ℝ))92 (hq : HeadTail.DependsOn S q) (hq1 : ∫ x, q x ∂haar = 1)93 (g : (dyadicSystem K rates).IntrinsicSpace)94 (hg : evalZero (dyadicSystem K rates).analysis g =95 multiplier K q (scalarCharacterLp K 1 ∅)) :96 intrinsicExpectation K rates m g = intrinsicCharacter K rates ∅ := by97 apply evalZero_injective (dyadicSystem K rates).analysis98 rw [evalZero_intrinsicExpectation, hg, expectation_multiplier_constant K m hS q hq hq1,99 evalZero_intrinsicCharacter]100101theorem norm_id_sub_intrinsicExpectation_le (rates : ℕ → ℝ≥0) (m : ℕ) :102 ‖ContinuousLinearMap.id K (dyadicSystem K rates).IntrinsicSpace -103 intrinsicExpectation K rates m‖ ≤ 2 := by104 have h := norm_sub_le (ContinuousLinearMap.id K (dyadicSystem K rates).IntrinsicSpace)105 (intrinsicExpectation K rates m)106 have hid := ContinuousLinearMap.norm_id_le (𝕜 := K)107 (E := (dyadicSystem K rates).IntrinsicSpace)108 linarith [norm_intrinsicExpectation_le K rates m]109110/-- Actual tail densities give the exact norm two of every complementary111coordinate projection. This proof uses the explicit spikes directly. -/112theorem norm_id_sub_intrinsicExpectation_eq_two_of_families (rates : ℕ → ℝ≥0)113 (hQ : ∀ (d : ℕ) (T : PositiveTime) (δ : ℝ), 0 < δ →114 Nonempty (TailSpikes.RateFamily rates d T δ)) (m : ℕ) :115 ‖ContinuousLinearMap.id K (dyadicSystem K rates).IntrinsicSpace -116 intrinsicExpectation K rates m‖ = 2 := by117 let P := ContinuousLinearMap.id K (dyadicSystem K rates).IntrinsicSpace -118 intrinsicExpectation K rates m119 have hup : ‖P‖ ≤ 2 := norm_id_sub_intrinsicExpectation_le K rates m120 have hlow (ε : ℝ) (hε : 0 < ε) : 2 - ε < ‖P‖ := by121 obtain ⟨T, hT⟩ := IntrinsicSpikes.exists_eta_lt (div_pos hε (by norm_num : (0:ℝ)<16))122 obtain ⟨Q⟩ := hQ m T (ε / 16) (by positivity)123 let c := intrinsicCharacter K rates ∅124 have hc : ‖c‖ = 1 := norm_intrinsicConstant K rates125 have hce : ‖evalZero (dyadicSystem K rates).analysis c‖ = 1 := by126 rw [evalZero_intrinsicCharacter, norm_constantL1]127 have hcV : c ∈ (intrinsicExpectation K rates m).range := intrinsicConstant_mem_range K rates m128 obtain ⟨g, hge, _havg, hgn, hgs⟩ := IntrinsicSpikeFamilies.exists_products Q (-c) c129 ((intrinsicExpectation K rates m).range.neg_mem hcV) hcV130 let a : FiniteCoordinateKernels.Assignments Q.coordinates := fun _ => 1131 have hgm : intrinsicExpectation K rates m (g a) = c := by132 apply intrinsicExpectation_tailProduct K rates m Q.beyond_prefix (Q.q a)133 (Q.q_depends a) (Q.integral_one a)134 simpa only [c, evalZero_intrinsicCharacter] using hge a135 have hgNorm : ‖g a‖ ≤ 1 + IntrinsicSpikes.eta T := by136 have hn := (abs_le.mp (hgn a)).2137 rw [hc, hce, mul_one] at hn138 linarith139 have hs : 2 - 4 * (ε / 16) - IntrinsicSpikes.eta T ≤ ‖P (g a)‖ := by140 have h := hgs a141 rw [norm_neg, hc, hce, mul_one] at h142 have hp : P (g a) = -c + g a := by143 simp only [P, sub_apply, ContinuousLinearMap.id_apply, hgm]144 abel145 rw [hp]146 nlinarith147 have hop := P.le_opNorm (g a)148 have hmul := mul_le_mul_of_nonneg_left hgNorm (norm_nonneg P)149 have herr := mul_le_mul_of_nonneg_right hup (IntrinsicSpikes.eta_pos T).le150 nlinarith151 apply le_antisymm hup152 by_contra h153 have he : 0 < (2 - ‖P‖) / 2 := by linarith154 have := hlow ((2 - ‖P‖) / 2) he155 linarith156157theorem schur_norm_id_sub_intrinsicExpectation_eq_two (m : ℕ) :158 ‖ContinuousLinearMap.id K (dyadicSystem K schurRates).IntrinsicSpace -159 intrinsicExpectation K schurRates m‖ = 2 :=160 norm_id_sub_intrinsicExpectation_eq_two_of_families K schurRates161 (fun d T _δ hδ => TailSpikes.exists_family d T hδ) m162163theorem constant_norm_id_sub_intrinsicExpectation_eq_two (m : ℕ) :164 ‖ContinuousLinearMap.id K (dyadicSystem K constantRates).IntrinsicSpace -165 intrinsicExpectation K constantRates m‖ = 2 :=166 norm_id_sub_intrinsicExpectation_eq_two_of_families K constantRates167 (fun d T _δ hδ => TailSpikes.exists_constant_family d T hδ) m168169end PL1.IntrinsicTailNorm170