PL1/IntrinsicSpikeAverages.lean

All source files · Download exact source

SHA-256: b759d5de014ea295356392ecad7e331eae3d55b4f55de4c8565c970708153b55

1import PL1.TailSpikes2import PL1.L1Multiplication3import PL1.IntrinsicGraph45/-! # Exact averages of actual intrinsic tail products -/67noncomputable section8open MeasureTheory9open scoped ENNReal NNReal BigOperators1011namespace PL1.IntrinsicSpikeAverages12open Walsh Noise IntrinsicGraph L1Multiplication1314variable (K : Type*) [RCLike K]1516theorem multiplier_real_smul (c : ℝ) (q : C(Walsh.Group, ℝ)) :17    multiplier K (c • q) = c • multiplier K q := by18  apply ContinuousLinearMap.ext19  intro f20  apply Lp.ext21  filter_upwards [coeFn_multiplier K (c • q) f, coeFn_multiplier K q f,22    Lp.coeFn_smul c (multiplier K q f)] with x hprod hq hsm23  change (multiplier K (c • q) f) x = (c • multiplier K q f) x24  rw [hprod, hsm]25  simp only [Pi.smul_apply]26  rw [hq]27  simp only [ContinuousMap.smul_apply, smul_eq_mul, smul_smul]2829def multiplierRealLinear : C(Walsh.Group, ℝ) →ₗ[ℝ]30    (Lp K 1 haar →L[K] Lp K 1 haar) where31  toFun := multiplier K32  map_add' := multiplier_add K33  map_smul' := multiplier_real_smul K3435theorem average_multipliers {rates : ℕ → ℝ≥0} {d : ℕ} {T : PositiveTime} {δ : ℝ}36    (Q : TailSpikes.RateFamily rates d T δ) :37    (Fintype.card (FiniteCoordinateKernels.Assignments Q.coordinates) : ℝ)⁻¹ •38        ∑ a, multiplier K (Q.q a) = ContinuousLinearMap.id K (Lp K 1 haar) := by39  have hq : (Fintype.card (FiniteCoordinateKernels.Assignments Q.coordinates) : ℝ)⁻¹ •40      ∑ a, Q.q a = (1 : C(Walsh.Group, ℝ)) := by41    ext x42    simpa only [ContinuousMap.smul_apply, ContinuousMap.sum_apply,43      ContinuousMap.one_apply, smul_eq_mul] using Q.average_one x44  have h := congrArg (multiplierRealLinear K) hq45  simpa only [map_smul, map_sum, multiplierRealLinear, LinearMap.coe_mk,46    AddHom.coe_mk, multiplier_one] using h4748theorem average_products {rates : ℕ → ℝ≥0} {d : ℕ} {T : PositiveTime} {δ : ℝ}49    (Q : TailSpikes.RateFamily rates d T δ)50    (D : ℕ → Lp K 1 haar →L[K] Lp K 1 haar) (f : Space D)51    (g : FiniteCoordinateKernels.Assignments Q.coordinates → Space D)52    (hg : ∀ a, evalZero D (g a) = multiplier K (Q.q a) (evalZero D f)) :53    (Fintype.card (FiniteCoordinateKernels.Assignments Q.coordinates) : ℝ)⁻¹ •54      ∑ a, g a = f := by55  apply evalZero_injective D56  let R := (evalZero D).restrictScalars ℝ57  change R (_ • ∑ a, g a) = R f58  rw [map_smul, map_sum]59  change _ • ∑ a, evalZero D (g a) = evalZero D f60  simp_rw [hg]61  have h := DFunLike.congr_fun (average_multipliers K Q) (evalZero D f)62  simpa only [smul_apply, sum_apply, ContinuousLinearMap.id_apply] using h6364end PL1.IntrinsicSpikeAverages65