enorm_czApproximation_le_infinite

lemma enorm_czApproximation_le_infinite {hf : BoundedFiniteSupport f} (hX : GeneralCase f α) :    ∀ᵐ x, ‖czApproximation f α x‖ₑ ≤ 2 ^ (3 * a) * α := by  have h₁ (x : X) (hx : ∃ i, x ∈ czPartition hX i) : ‖czApproximation f α x‖ₑ ≤ 2 ^ (3 * a) * α :=    have ⟨i, hi⟩ := hx    calc ‖czApproximation f α x‖ₑ      _ = ‖⨍ x in czPartition hX i, f x‖ₑ := by rw [czApproximation_def_of_mem hi]      _ ≤ ⨍⁻ x in czPartition hX i, ‖f x‖ₑ ∂volume := enorm_integral_le_lintegral_enorm _      _ ≤ (volume (czPartition hX i))⁻¹ * ∫⁻ x in czPartition hX i, ‖f x‖ₑ := by        simp [laverage]      _ ≤ 2 ^ (3 * a) * (volume (czBall7 hX i))⁻¹ * ∫⁻ x in czPartition hX i, ‖f x‖ₑ := by        apply mul_le_mul_left        have := (ENNReal.inv_mul_le_iff (by simp) (by simp)).mpr <| volume_czBall7_le hX i        rwa [← ENNReal.inv_le_inv, ENNReal.mul_inv (by simp) (by simp), inv_inv] at this      _ ≤ 2 ^ (3 * a) * (volume (czBall7 hX i))⁻¹ * ∫⁻ x in czBall7 hX i, ‖f x‖ₑ :=        mul_le_mul_right (lintegral_mono_set czPartition_subset_czBall7) _      _ ≤ 2 ^ (3 * a) * α := by        rw [mul_assoc]; gcongr; simpa [laverage] using laverage_czBall7_le hX i  have h₂ : ∀ᵐ x, ¬(∃ i, x ∈ czPartition hX i) → ‖czApproximation f α x‖ₑ ≤ 2 ^ (3 * a) * α :=    (lebesgue_differentiation hf).mono fun x ⟨c, r, lim, _, x_mem_ball⟩ hx ↦ by      have le_α := hx      rw [← mem_iUnion, iUnion_czPartition, mem_preimage, mem_Ioi, not_lt] at le_α      simp only [czApproximation, hX, reduceDIte, hx]      refine le_of_tendsto lim.enorm <| Eventually.of_forall fun i ↦ ?_      apply le_trans (enorm_integral_le_lintegral_enorm f)      exact le_trans (laverage_le_globalMaximalFunction (x_mem_ball i)) <| le_α.trans α_le_mul_α  simpa only [← or_imp, em, forall_const] using eventually_and.mpr ⟨Eventually.of_forall h₁, h₂⟩