PL1/InputCompression.lean
All source files · Download exact source
SHA-256: e57983a9a6ea43d5bff8c8482125e1dc7fbbb84fac41aeff3d64704630750edd
1import PL1.MatrixTrace2import PL1.IntervalModel34/-! # Uniform finite-coordinate approximation of bounded interval inputs -/56noncomputable section7set_option autoImplicit false8set_option maxHeartbeats 8000009set_option backward.isDefEq.respectTransparency false10open MeasureTheory Filter11open scoped ENNReal BigOperators Topology1213namespace PL1.InputCompression1415attribute [local instance] DyadicTrace.intervalMeasure_probability1617variable {𝕜 Ω : Type*} [RCLike 𝕜] [MeasurableSpace Ω] (μ : Measure Ω)1819theorem norm_mask_compl_restriction_tendsto_zero20 (B : IntervalL1 𝕜 →L[𝕜] Lp 𝕜 1 μ)21 (A : ℕ → Set Ω) (hA : ∀ n, MeasurableSet (A n))22 (hcover : ∀ x, ∀ᶠ n : ℕ in atTop, x ∈ A n) :23 Tendsto (fun n => ‖(L1Masks.mask μ (A n)ᶜ (hA n).compl).comp24 (OperatorDomination.restriction μ B)‖) atTop (𝓝 0) := by25 obtain ⟨G, hG, hGint, hGpos, _, hdom⟩ := OperatorDomination.exists_measurable_dominator μ B26 have ht : Tendsto (fun n => ∫ x in (A n)ᶜ, G x ∂μ) atTop (𝓝 0) := by27 have h := tendsto_integral_of_dominated_convergence (μ := μ) (f := fun _ => (0 : ℝ)) G28 (fun n => (hG.indicator (hA n).compl).aestronglyMeasurable) hGint29 (fun n => ae_of_all _ (fun x => by30 by_cases hx : x ∈ (A n)ᶜ31 · rw [Set.indicator_of_mem hx, Real.norm_eq_abs, abs_of_nonneg (hGpos x)]32 · rw [Set.indicator_of_notMem hx, norm_zero]33 exact hGpos x))34 (ae_of_all _ (fun x => by35 apply tendsto_const_nhds.congr'36 filter_upwards [hcover x] with n hn37 exact (Set.indicator_of_notMem (show x ∉ (A n)ᶜ from fun h => h hn) G).symm))38 simpa only [integral_indicator (hA _).compl, integral_zero] using h39 exact squeeze_zero (fun n => norm_nonneg _)40 (fun n => OperatorDomination.norm_mask_restriction_le μ B G hGint hGpos hdom _ _) ht4142variable [SFinite μ]4344def components (n : ℕ) : Set (ℕ × Ω) := {x | x.1 < n}4546theorem measurableSet_components (n : ℕ) : MeasurableSet (components (Ω := Ω) n) :=47 measurable_fst (measurableSet_lt measurable_id measurable_const)4849theorem flatten_compression (n : ℕ) (x : L1Sum (Lp 𝕜 1 μ)) :50 IntervalModel.flatten μ (MatrixTrace.compression (𝕜 := 𝕜) (Finset.range n) x) =51 L1Masks.mask (IntervalModel.disjointMeasure μ) (components n) (measurableSet_components n)52 (IntervalModel.flatten μ x) := by53 apply Lp.ext54 apply (IntervalModel.flatten_coeFn μ _).trans55 apply Filter.EventuallyEq.trans _56 (L1Masks.coeFn_mask (IntervalModel.disjointMeasure μ) (components n)57 (measurableSet_components n) (IntervalModel.flatten μ x)).symm58 have hflat := IntervalModel.flatten_coeFn μ x59 apply Filter.EventuallyEq.trans _ (hflat.indicator (s := components n)).symm60 change IntervalModel.flattenFunction μ (MatrixTrace.compression (𝕜 := 𝕜) (Finset.range n) x) =ᵐ[61 Measure.count.prod μ] (components n).indicator (IntervalModel.flattenFunction μ x)62 apply (Measure.ae_prod_iff_ae_ae (measurableSet_eq_fun63 (IntervalModel.measurable_flattenFunction μ _)64 ((IntervalModel.measurable_flattenFunction μ x).indicator (measurableSet_components n)))).mpr65 exact ae_of_all _ (fun i => by66 by_cases hi : i < n67 · exact ae_of_all _ (fun z => by68 simp only [IntervalModel.flattenFunction, MatrixTrace.compression_apply_coord,69 Finset.mem_range, hi, ite_true, components, Set.indicator_of_mem70 (show (i, z) ∈ {x : ℕ × Ω | x.1 < n} from hi)])71 · filter_upwards [Lp.coeFn_zero (E := 𝕜) (p := 1) (μ := μ)] with z hz72 simp only [IntervalModel.flattenFunction, MatrixTrace.compression_apply_coord,73 Finset.mem_range, hi, ite_false, components, Set.indicator_of_notMem74 (show (i, z) ∉ {x : ℕ × Ω | x.1 < n} from hi)]75 exact hz)7677theorem norm_input_compression_error_tendsto_zero78 (B : IntervalL1 𝕜 →L[𝕜] L1Sum (Lp 𝕜 1 μ)) :79 Tendsto (fun n => ‖((ContinuousLinearMap.id 𝕜 (L1Sum (Lp 𝕜 1 μ)) -80 MatrixTrace.compression (𝕜 := 𝕜) (Finset.range n)).comp B).comp81 (ProbabilityLp.inclusion intervalMeasure 1 ∞ le_top)‖) atTop (𝓝 0) := by82 let e := IntervalModel.sumDisjointEquiv (𝕜 := 𝕜) μ83 have ht := norm_mask_compl_restriction_tendsto_zero (IntervalModel.disjointMeasure μ)84 ((e : L1Sum (Lp 𝕜 1 μ) →L[𝕜] Lp 𝕜 1 (IntervalModel.disjointMeasure μ)).comp B)85 components measurableSet_components (fun x => eventually_gt_atTop x.1)86 have heq (n : ℕ) : (L1Masks.mask (IntervalModel.disjointMeasure μ) (components n)ᶜ87 (measurableSet_components n).compl).comp88 (OperatorDomination.restriction (IntervalModel.disjointMeasure μ)89 ((e : L1Sum (Lp 𝕜 1 μ) →L[𝕜] Lp 𝕜 1 (IntervalModel.disjointMeasure μ)).comp B)) =90 (e : L1Sum (Lp 𝕜 1 μ) →L[𝕜] Lp 𝕜 1 (IntervalModel.disjointMeasure μ)).comp91 (((ContinuousLinearMap.id 𝕜 (L1Sum (Lp 𝕜 1 μ)) - MatrixTrace.compression (Finset.range n)).comp B).comp92 (ProbabilityLp.inclusion intervalMeasure 1 ∞ le_top)) := by93 rw [← OperatorDomination.mask_compl (IntervalModel.disjointMeasure μ)94 (components n) (measurableSet_components n)]95 apply ContinuousLinearMap.ext96 intro f97 simp only [ContinuousLinearMap.comp_apply, sub_apply, ContinuousLinearMap.id_apply,98 OperatorDomination.restriction, map_sub]99 exact congrArg (fun z => e (B (ProbabilityLp.inclusion intervalMeasure 1 ∞ le_top f)) - z)100 (flatten_compression μ n (B (ProbabilityLp.inclusion intervalMeasure 1 ∞ le_top f))).symm101 simpa only [heq, ContinuousLinearMap.opNorm_linearIsometryEquiv_comp] using ht102103end PL1.InputCompression104