measurable_T_lin

lemma measurable_T_lin (mf : Measurable f) (mσ₁ : Measurable σ₁) (mσ₂ : Measurable σ₂)    (rσ₁ : (range σ₁).Finite) (rσ₂ : (range σ₂).Finite) : Measurable (T_lin Q σ₁ σ₂ f ·) := by  obtain ⟨lb, hlb⟩ := bddBelow_def.mp rσ₁.bddBelow  obtain ⟨ub, hub⟩ := bddAbove_def.mp rσ₂.bddAbove  simp_rw [mem_range, forall_exists_index, forall_apply_eq_imp_iff] at hlb hub  have rearr : T_lin Q σ₁ σ₂ f = fun x ↦ ∑ s ∈ Finset.Icc lb ub,      {x' | s ∈ Icc (σ₁ x') (σ₂ x')}.indicator        (fun z ↦ ∫ y, Ks s z y * f y * exp (I * Q z y)) x := by    ext x; unfold T_lin T_S    calc      _ = ∑ s ∈ Finset.Icc (σ₁ x) (σ₂ x), {x' | s ∈ Icc (σ₁ x') (σ₂ x')}.indicator          (fun z ↦ ∫ y, Ks s z y * f y * exp (I * Q z y)) x := by        congr! with s ms; rw [indicator_of_mem (by simpa using ms)]      _ = _ := by        refine Finset.sum_subset (Finset.Icc_subset_Icc (hlb x) (hub x)) fun s ms ns ↦ ?_        apply indicator_of_notMem; rwa [mem_setOf_eq, mem_Icc, ← Finset.mem_Icc]  rw [rearr]  refine Finset.measurable_sum _ fun _ _ ↦ (measurable_T_inner_integral mf).indicator ?_  rw [measurableSet_setOf]; apply (measurable_set_mem _).comp  apply Measurable.comp (f := fun x ↦ (σ₁ x, σ₂ x)) (g := fun p ↦ Icc p.1 p.2)  · exact measurable_from_prod_countable_left fun _ _ _ ↦ trivial  · exact mσ₁.prodMk mσ₂