PL1/IntrinsicSpikeFamilies.lean
All source files · Download exact source
SHA-256: e6a75374a81ffbcd1504f7543b8cc0aa67f2c53e549fc4a2bec43423ff122872
1import PL1.IntrinsicHeadRepresentatives2import PL1.IntrinsicSpikeAverages3import PL1.IntrinsicSpikes4import PL1.TailSpikeMultiplication5import PL1.DaugavetAveraging67/-!8# Actual finite spike families in the intrinsic space910Finite head representatives, genuine tail families, Haar independence and the11proved resolvent commutator discharge every input to the intrinsic coordinate12estimates. The resulting family lives in the original dyadic intrinsic graph.13-/1415noncomputable section16open MeasureTheory17open scoped ENNReal NNReal BigOperators1819namespace PL1.IntrinsicSpikeFamilies20open Noise Walsh IntrinsicGraph IntrinsicHeadRepresentatives21open FiniteCoordinateKernels L1Multiplication2223variable {K : Type*} [RCLike K]2425theorem coordinate_norm_preserved {rates : ℕ → ℝ≥0} {d : ℕ}26 {T : PositiveTime} {δ : ℝ} (Q : TailSpikes.RateFamily rates d T δ)27 (a : Assignments Q.coordinates) {f : (dyadicSystem K rates).IntrinsicSpace}28 (hf : f ∈ (intrinsicExpectation K rates d).range) (n : ℕ) :29 ‖multiplier K (Q.q a) (coord (dyadicSystem K rates).analysis n f)‖ =30 ‖coord (dyadicSystem K rates).analysis n f‖ := by31 obtain ⟨F, hF, hFeq⟩ := continuousRepresentative_coord_of_range rates d n hf32 rw [← hFeq]33 exact HeadTail.norm_multiplier_toLp_of_density Q.beyond_prefix.symm F (Q.q a)34 hF (Q.q_depends a) (ae_of_all _ (Q.nonnegative a)) (Q.integral_one a)3536theorem coordinate_separation {rates : ℕ → ℝ≥0} {d : ℕ}37 {T : PositiveTime} {δ : ℝ} (Q : TailSpikes.RateFamily rates d T δ)38 (a : Assignments Q.coordinates) {h f : (dyadicSystem K rates).IntrinsicSpace}39 (hh : h ∈ (intrinsicExpectation K rates d).range)40 (hf : f ∈ (intrinsicExpectation K rates d).range) (n : ℕ) :41 (1 - 2 * δ) * (‖coord (dyadicSystem K rates).analysis n h‖ +42 ‖coord (dyadicSystem K rates).analysis n f‖) ≤43 ‖coord (dyadicSystem K rates).analysis n h +44 multiplier K (Q.q a) (coord (dyadicSystem K rates).analysis n f)‖ := by45 obtain ⟨H, hH, hHeq⟩ := continuousRepresentative_coord_of_range rates d n hh46 obtain ⟨F, hF, hFeq⟩ := continuousRepresentative_coord_of_range rates d n hf47 rw [← hHeq, ← hFeq]48 exact HeadTail.concentration_multiplier_toLp Q.beyond_prefix.symm H F (Q.q a)49 hH hF (Q.q_depends a) (ae_of_all _ (Q.nonnegative a)) (Q.integral_one a)50 (Q.B a) (Q.measurable a) δ (Q.small a).le (Q.concentrated a).le5152theorem coordinate_commutator {rates : ℕ → ℝ≥0} {d : ℕ}53 {T : PositiveTime} {δ : ℝ} (Q : TailSpikes.RateFamily rates d T δ)54 (a : Assignments Q.coordinates) {f : (dyadicSystem K rates).IntrinsicSpace}55 (hf : f ∈ (intrinsicExpectation K rates d).range) :56 ∀ n, ‖(dyadicSystem K rates).analysis n57 (multiplier K (Q.q a) (evalZero (dyadicSystem K rates).analysis f)) -58 multiplier K (Q.q a) (coord (dyadicSystem K rates).analysis n f)‖ ≤59 IntrinsicSpikes.error T ‖evalZero (dyadicSystem K rates).analysis f‖ n := by60 apply IntrinsicSpikes.coordinate_commutator_le rates (multiplier K (Q.q a)) f T61 obtain ⟨F, hF, hFeq⟩ := continuousRepresentative_evalZero_of_range rates d hf62 intro t63 rw [← hFeq]64 exact Q.norm_id_sub_resolvent_commutator_le a F hF t6566/-- The actual products have exact finite average, the manuscript's norm bound,67and its separation estimate, without residual analytic assumptions. -/68theorem exists_products {rates : ℕ → ℝ≥0} {d : ℕ}69 {T : PositiveTime} {δ : ℝ} (Q : TailSpikes.RateFamily rates d T δ)70 (h f : (dyadicSystem K rates).IntrinsicSpace)71 (hh : h ∈ (intrinsicExpectation K rates d).range)72 (hf : f ∈ (intrinsicExpectation K rates d).range) :73 ∃ g : Assignments Q.coordinates → (dyadicSystem K rates).IntrinsicSpace,74 (∀ a, evalZero (dyadicSystem K rates).analysis (g a) =75 multiplier K (Q.q a) (evalZero (dyadicSystem K rates).analysis f)) ∧76 (Fintype.card (Assignments Q.coordinates) : K)⁻¹ • (∑ a, g a) = f ∧77 (∀ a, |‖g a‖ - ‖f‖| ≤78 IntrinsicSpikes.eta T * ‖evalZero (dyadicSystem K rates).analysis f‖) ∧79 (∀ a, (1 - 2 * δ) * (‖h‖ + ‖f‖) -80 IntrinsicSpikes.eta T * ‖evalZero (dyadicSystem K rates).analysis f‖ ≤ ‖h + g a‖) := by81 have hex (a : Assignments Q.coordinates) := IntrinsicSpikes.exists_product rates82 (multiplier K (Q.q a)) f T (coordinate_norm_preserved Q a hf)83 (coordinate_commutator Q a hf)84 choose g hge hgn using hex85 refine ⟨g, hge, ?_, hgn, ?_⟩86 · have havg := IntrinsicSpikeAverages.average_products K Q (dyadicSystem K rates).analysis f g hge87 have hsmul : (Fintype.card (Assignments Q.coordinates) : ℝ)⁻¹ • (∑ a, g a) =88 (((Fintype.card (Assignments Q.coordinates) : ℝ)⁻¹ : ℝ) : K) • (∑ a, g a) := by89 apply Subtype.ext90 change (Fintype.card (Assignments Q.coordinates) : ℝ)⁻¹ •91 ((∑ a, g a : (dyadicSystem K rates).IntrinsicSpace) : Ambient (Y := Lp K 1 haar)) =92 (((Fintype.card (Assignments Q.coordinates) : ℝ)⁻¹ : ℝ) : K) •93 ((∑ a, g a : (dyadicSystem K rates).IntrinsicSpace) : Ambient (Y := Lp K 1 haar))94 exact RCLike.real_smul_eq_coe_smul (K := K) _ _95 rw [hsmul] at havg96 simpa only [RCLike.ofReal_inv, RCLike.ofReal_natCast] using havg97 · intro a98 exact IntrinsicSpikes.separation rates (multiplier K (Q.q a)) h f (g a) (hge a) T δ99 (coordinate_separation Q a hh hf) (coordinate_commutator Q a hf)100101/-- Existence of genuine tail families supplies exactly the finite-family102criterion on the original finite-coordinate intrinsic ranges. -/103theorem finiteSpikeFamilies (rates : ℕ → ℝ≥0)104 (hQ : ∀ (d : ℕ) (T : PositiveTime) (δ : ℝ), 0 < δ →105 Nonempty (TailSpikes.RateFamily rates d T δ)) :106 Daugavet.FiniteSpikeFamilies K (dyadicSystem K rates).IntrinsicSpace107 (fun n => (intrinsicExpectation K rates n).range) := by108 classical109 intro d h hh f hf δ hδ η hη110 obtain ⟨T, hT⟩ := IntrinsicSpikes.exists_eta_lt hη111 obtain ⟨Q⟩ := hQ d T δ hδ112 obtain ⟨g, hge, havg, hgn, hgs⟩ := exists_products Q h f hh hf113 let e := Fintype.equivFin (Assignments Q.coordinates)114 refine ⟨Fintype.card (Assignments Q.coordinates), Fintype.card_pos, fun i => g (e.symm i),115 ?_, ?_, ?_⟩116 · rw [e.symm.sum_comp]117 exact havg118 · intro a119 have he : IntrinsicSpikes.eta T * ‖evalZero (dyadicSystem K rates).analysis f‖ ≤120 η * ‖f‖ := mul_le_mul hT.le (norm_evalZero_le _ _) (norm_nonneg _) hη.le121 have hn := (abs_le.mp (hgn (e.symm a))).2122 nlinarith123 · intro a124 have he : IntrinsicSpikes.eta T * ‖evalZero (dyadicSystem K rates).analysis f‖ ≤125 η * ‖f‖ := mul_le_mul hT.le (norm_evalZero_le _ _) (norm_nonneg _) hη.le126 linarith [hgs (e.symm a)]127128end PL1.IntrinsicSpikeFamilies129