Crossover estimate unaveraged

theorem crossover_estimate_unaveraged    (hd : 2 < (d : ℝ))    (A : NormalizedEllipticCoeff d (Metric.ball (0 : E) 1))    {u : E → ℝ}    (hu_pos : ∀ x ∈ Metric.ball (0 : E) 1, 0 < u x)    (hsuper : IsSupersolution A.1 u) :    (∫ x in Metric.ball (0 : E) (1 / 2 : ℝ),        |u x| ^ (c_crossover' d / A.1.Λ ^ ((1 : ℝ) / 2)) ∂volume) *      (∫ x in Metric.ball (0 : E) (1 / 2 : ℝ),        |u x| ^ (-(c_crossover' d / A.1.Λ ^ ((1 : ℝ) / 2))) ∂volume) ≤        C_crossover' d *          (volume.real (Metric.ball (0 : E) (1 / 2 : ℝ))) ^ 2 := by  let B : Set E := Metric.ball (0 : E) (1 / 2 : ℝ)  set p₀ : ℝ := c_crossover' d / A.1.Λ ^ ((1 : ℝ) / 2)  set Ipos : ℝ := ∫ x in B, |u x| ^ p₀ ∂volume  set Ineg : ℝ := ∫ x in B, |u x| ^ (-p₀) ∂volume  have havg := crossover_estimate (d := d) hd A hu_pos hsuper  have hvol_pos : 0 < volume.real B := by    exact ENNReal.toReal_pos      (measure_ball_pos volume (0 : E) (by norm_num : (0 : ℝ) < 1 / 2)).ne'      measure_ball_lt_top.ne  have hvol_ne : volume.real B ≠ 0 := ne_of_gt hvol_pos  have hscale_nonneg : 0 ≤ (volume.real B) ^ 2 := by positivity  rw [MeasureTheory.setAverage_eq, MeasureTheory.setAverage_eq, smul_eq_mul, smul_eq_mul] at havg  have hscaled :=    mul_le_mul_of_nonneg_left havg hscale_nonneg  calc    Ipos * Ineg        = (volume.real B) ^ 2 * ((volume.real B)⁻¹ * Ipos * ((volume.real B)⁻¹ * Ineg)) := by            field_simp [hvol_ne]    _ ≤ (volume.real B) ^ 2 * C_crossover' d := hscaled    _ = C_crossover' d * (volume.real B) ^ 2 := by ring