Tile.boundedCompactSupport_star_Ks_mul_g

lemma boundedCompactSupport_star_Ks_mul_g {p' : 𝔓 X} {g : X → ℂ}    (hg : Measurable g) (hg1 : ∀ x, ‖g x‖ ≤ G.indicator 1 x) :    BoundedCompactSupport fun x : X × X ↦ conj (Ks (𝔰 p') x.1 x.2) * g x.1 := by  apply BoundedCompactSupport.mul_bdd_left' (bcs_of_measurable_of_le_indicator_g hg hg1)    continuous_fst  · exact quasiMeasurePreserving_fst  · fun_prop  · intros K hK    obtain ⟨C, hC⟩ := isBounded_iff.1 hK.isBounded    apply isCompact_of_isClosed_isBounded      ((IsClosed.preimage continuous_fst hK.isClosed).inter (isClosed_tsupport _))    rw [isBounded_iff]    use D ^ 𝔰 p' + C    intros x hx y hy    rw [Prod.dist_eq, sup_le_iff]    constructor    · calc        _ ≤ _ := hC hx.1 hy.1        _ ≤ _ := le_add_of_nonneg_left (by positivity)    · calc        _ ≤ dist x.2 x.1 + dist x.1 y.1 + dist y.1 y.2 := dist_triangle4 ..        _ ≤ D ^ 𝔰 p' / 2 + C + D ^ 𝔰 p' / 2 := by          gcongr          · rw [dist_comm]            have hx' : x ∈ tsupport fun x ↦ Ks (𝔰 p') x.1 x.2 := by              convert hx.2 using 1              simp only [tsupport]              apply congr_arg              ext z              simp only [mem_support, ne_eq, map_eq_zero]            exact (dist_mem_Icc_of_mem_tsupport_Ks hx').2          · exact hC hx.1 hy.1          · have hy' : y ∈ tsupport fun x ↦ Ks (𝔰 p') x.1 x.2 := by              convert hy.2 using 1              simp only [tsupport]              apply congr_arg              ext z              simp only [mem_support, ne_eq, map_eq_zero]            exact (dist_mem_Icc_of_mem_tsupport_Ks hy').2        _ = _ := by ring  · intro A hA; rw [isBounded_image_iff]    obtain ⟨C, hC0, hC⟩ := Bornology.IsBounded.exists_bound_of_norm_Ks hA (𝔰 p')    use C + C; intro x hx y hy; rw [dist_conj_conj]    calc      _ ≤ _ := dist_le_norm_add_norm ..      _ ≤ _ := add_le_add (hC x.1 x.2 hx) (hC y.1 y.2 hy)