TileStructure.Forest.boundary_operator_bound

lemma boundary_operator_bound (hf : BoundedCompactSupport f) :    eLpNorm (t.boundaryOperator u f) 2 volume ≤ C7_2_3 a * eLpNorm f 2 volume := by  have bcs : BoundedCompactSupport fun x ↦ (t.boundaryOperator u f x).toReal := by    simp_rw [e728_push_toReal hf]    refine BoundedCompactSupport.finset_sum fun I _ ↦ ?_    refine BoundedCompactSupport.indicator_of_isCompact_closure (memLp_top_const _)      (Metric.isBounded_ball.subset Grid_subset_ball).isCompact_closure coeGrid_measurable  have elpn_eq : eLpNorm (fun x ↦ (t.boundaryOperator u f x).toReal) 2 volume =      eLpNorm (t.boundaryOperator u f) 2 volume :=    eLpNorm_toReal_eq (Eventually.of_forall fun _ ↦ (boundaryOperator_lt_top hf).ne)  by_cases hv : eLpNorm (t.boundaryOperator u f) 2 volume = 0; · simp [hv]  have hv' : eLpNorm (t.boundaryOperator u f) 2 volume < ⊤ := elpn_eq ▸ (bcs.memLp 2).2  rw [← ENNReal.mul_le_mul_iff_left hv hv'.ne, ← sq, ← ENNReal.rpow_natCast]  nth_rw 1 [show ((2 : ℕ) : ℝ) = (2 : ℝ≥0) by rfl, show (2 : ℝ≥0∞) = (2 : ℝ≥0) by rfl,    eLpNorm_nnreal_pow_eq_lintegral two_ne_zero]  convert boundary_operator_bound_aux (t := t) (u := u) hf bcs.toComplex using 2  · simp_rw [RCLike.conj_mul]; norm_cast    simp_rw [← norm_pow, integral_norm_eq_lintegral_enorm      (bcs.aestronglyMeasurable.aemeasurable.pow_const 2).aestronglyMeasurable, enorm_pow,      Real.enorm_toReal (boundaryOperator_lt_top hf).ne, enorm_eq_self]    simp_rw [enorm_eq_nnnorm, coe_algebraMap, nnnorm_real, ← enorm_eq_nnnorm,      ← ENNReal.rpow_natCast, Nat.cast_ofNat]    refine (Real.enorm_toReal ?_).symm    replace hv' := ENNReal.pow_lt_top (n := 2) hv'    rw [← ENNReal.rpow_natCast, show ((2 : ℕ) : ℝ) = (2 : ℝ≥0) by rfl,      show (2 : ℝ≥0∞) = (2 : ℝ≥0) by rfl, eLpNorm_nnreal_pow_eq_lintegral two_ne_zero,      show ((2 : ℝ≥0) : ℝ) = (2 : ℕ) by rfl] at hv'    simp_rw [enorm_eq_self] at hv'; exact hv'.ne  · rw [← elpn_eq, show (2 : ℝ≥0∞) = (2 : ℝ≥0) by rfl]    simp_rw [eLpNorm_nnreal_eq_lintegral two_ne_zero]; congr!    simp [enorm_eq_nnnorm, nnnorm_real]