TileStructure.Forest.boundedCompactSupport_toReal_χ

lemma boundedCompactSupport_toReal_χ (hJ : J ∈ 𝓙₅ t u₁ u₂) :    BoundedCompactSupport fun x ↦ (χ t u₁ u₂ J x : ℝ) := by  apply BoundedCompactSupport.mono_norm (g := fun x ↦ (ball (c J) (8 * D ^ s J)).indicator 1 x)    ?_ ?_ (fun x ↦ ?_)  · constructor    · refine memLp_top_of_bound (by fun_prop (discharger := measurability)) 1 (.of_forall fun x ↦ ?_)      unfold indicator; split_ifs <;> simp    · refine HasCompactSupport.intro (isCompact_closedBall (c J) (8 * D ^ s J)) fun x mx ↦ ?_      apply indicator_of_notMem; contrapose! mx; exact ball_subset_closedBall mx  · exact stronglyMeasurable_χ.measurable.coe_nnreal_real.aestronglyMeasurable  · simp_rw [show (1 : X → ℝ) = (↑) ∘ (1 : X → ℝ≥0) by rfl]    rw [indicator_comp_of_zero (by simp), Function.comp_apply, Real.norm_eq_abs, NNReal.abs_eq,      NNReal.coe_le_coe]    exact χ_le_indicator hJ