John nirenberg level set decay

theorem john_nirenberg_level_set_decay    {x₀ : E} {r : ℝ} {E_lam E_lam_A : Set E}    {ι : Type*} [Countable ι] (B : ι → JNBall x₀ r)    (_hE_lam_meas : MeasurableSet E_lam)    (hE_lam_A_meas : MeasurableSet E_lam_A)    (hE_lam_fin : volume E_lam ≠ ⊤)    (hE_lam_A_sub : E_lam_A ⊆ E_lam)    (hcover : E_lam ⊆ ⋃ i, (B i).fivefold)    (hU_sub_E_lam : (⋃ i, (B i).carrier) ⊆ E_lam)    (hdisj : ∀ i j, i ≠ j → Disjoint ((B i).carrier) ((B j).carrier))    (hmain : ∀ i,      volume (E_lam_A ∩ (B i).carrier) ≤ ENNReal.ofReal (1 / 2) * volume ((B i).carrier)) :    volume.real E_lam_A ≤ (1 - 1 / (2 * 5 ^ d)) * volume.real E_lam := by  -- Finiteness of derived sets  have hE_lam_A_fin : volume E_lam_A ≠ ⊤ := measure_ne_top_of_subset hE_lam_A_sub hE_lam_fin  -- Set up U = ⋃ i, (B i).carrier  set U := ⋃ i, (B i).carrier with hU_def  have hU_meas : MeasurableSet U :=    MeasurableSet.iUnion (fun i => (B i).measurableSet_carrier)  have hU_fin : volume U ≠ ⊤ := measure_ne_top_of_subset hU_sub_E_lam hE_lam_fin  -- Carrier finiteness  have hcarrier_fin : ∀ i, volume ((B i).carrier) ≠ ⊤ :=    fun i => measure_ne_top_of_subset (subset_iUnion (fun i => (B i).carrier) i) hU_fin  -- Pairwise disjointness in Pairwise form  have hdisj_pw : Pairwise (Function.onFun Disjoint fun i => (B i).carrier) :=    fun i j hij => hdisj i j hij  have hvolU : volume U = ∑' i, volume ((B i).carrier) :=    measure_iUnion hdisj_pw (fun i => (B i).measurableSet_carrier)  have hE_lam_le : volume.real E_lam ≤ (5 : ℝ) ^ d * volume.real U := by    have h1 : volume E_lam ≤ volume (⋃ i, (B i).fivefold) := measure_mono hcover    have h2 : volume (⋃ i, (B i).fivefold) ≤ ∑' i, volume ((B i).fivefold) :=      measure_iUnion_le _    have h3 : ∀ i, volume ((B i).fivefold) = ENNReal.ofReal ((5 : ℝ) ^ d) * volume ((B i).carrier) :=      fun i => (B i).volume_fivefold    have h4 : ∑' i, volume ((B i).fivefold) = ∑' i, (ENNReal.ofReal ((5 : ℝ) ^ d) * volume ((B i).carrier)) :=      tsum_congr (fun i => h3 i)    have h5 : ∑' i, (ENNReal.ofReal ((5 : ℝ) ^ d) * volume ((B i).carrier)) =        ENNReal.ofReal ((5 : ℝ) ^ d) * ∑' i, volume ((B i).carrier) :=      ENNReal.tsum_mul_left    rw [h4, h5, ← hvolU] at h2    have hfive_ne_top : ENNReal.ofReal ((5 : ℝ) ^ d) * volume U ≠ ⊤ :=      ENNReal.mul_ne_top ENNReal.ofReal_ne_top hU_fin    have hle := ENNReal.toReal_mono hfive_ne_top (h1.trans h2)    rwa [ENNReal.toReal_mul, ENNReal.toReal_ofReal (by positivity : (0:ℝ) ≤ (5:ℝ) ^ d)] at hle  have hA_inter_U : volume.real (E_lam_A ∩ U) ≤ 1 / 2 * volume.real U := by    -- Work in ENNReal: volume (E_lam_A ∩ U) ≤ ENNReal.ofReal (1/2) * volume U    have hinter_eq : E_lam_A ∩ U = ⋃ i, (E_lam_A ∩ (B i).carrier) := by      simp [hU_def, inter_iUnion]    have hdisj_inter : Pairwise (Function.onFun Disjoint fun i => E_lam_A ∩ (B i).carrier) := by      intro i j hij      exact Disjoint.mono inter_subset_right inter_subset_right (hdisj_pw hij)    have hmeas_inter : ∀ i, MeasurableSet (E_lam_A ∩ (B i).carrier) :=      fun i => hE_lam_A_meas.inter (B i).measurableSet_carrier    have hvol_inter : volume (E_lam_A ∩ U) = ∑' i, volume (E_lam_A ∩ (B i).carrier) := by      rw [hinter_eq, measure_iUnion hdisj_inter hmeas_inter]    have henn_le : volume (E_lam_A ∩ U) ≤ ENNReal.ofReal (1 / 2) * volume U := by      rw [hvol_inter, hvolU]      calc ∑' i, volume (E_lam_A ∩ (B i).carrier)          ≤ ∑' i, (ENNReal.ofReal (1 / 2) * volume ((B i).carrier)) :=            ENNReal.tsum_le_tsum (fun i => hmain i)        _ = ENNReal.ofReal (1 / 2) * ∑' i, volume ((B i).carrier) :=            ENNReal.tsum_mul_left    have hfin : ENNReal.ofReal (1 / 2) * volume U ≠ ⊤ :=      ENNReal.mul_ne_top ENNReal.ofReal_ne_top hU_fin    have := ENNReal.toReal_mono hfin henn_le    rwa [ENNReal.toReal_mul, ENNReal.toReal_ofReal (by norm_num : (0:ℝ) ≤ 1/2)] at this  have hAdiffU_sub : E_lam_A \ U ⊆ E_lam \ U :=    diff_subset_diff_left hE_lam_A_sub  -- volume.real E_lam_A = volume.real (E_lam_A ∩ U) + volume.real (E_lam_A \ U)  have hE_lam_A_split : volume.real E_lam_A =      volume.real (E_lam_A ∩ U) + volume.real (E_lam_A \ U) := by    rw [← measureReal_inter_add_diff hU_meas hE_lam_A_fin]  -- volume.real (E_lam \ U) = volume.real E_lam - volume.real U  have hE_lam_diff : volume.real (E_lam \ U) = volume.real E_lam - volume.real U :=    measureReal_diff hU_sub_E_lam hU_meas hE_lam_fin  -- volume.real (E_lam_A \ U) ≤ volume.real (E_lam \ U)  have hAdiffU_le : volume.real (E_lam_A \ U) ≤ volume.real (E_lam \ U) := by    exact measureReal_mono hAdiffU_sub      (ne_top_of_le_ne_top hE_lam_fin (measure_mono diff_subset))  have hU_lower : 1 / (5 : ℝ) ^ d * volume.real E_lam ≤ volume.real U := by    by_cases h5d : (5 : ℝ) ^ d = 0    · simp [h5d]    · rw [div_mul_eq_mul_div, one_mul]      exact div_le_of_le_mul₀ (by positivity) measureReal_nonneg (by linarith [hE_lam_le])  -- Now combine: volume.real E_lam_A ≤ 1/2 * volume.real U + (volume.real E_lam - volume.real U)  --                                    = volume.real E_lam - 1/2 * volume.real U  --                                    ≤ volume.real E_lam - 1/2 * 1/5^d * volume.real E_lam  --                                    = (1 - 1/(2*5^d)) * volume.real E_lam  have hU_real_le : volume.real U ≤ volume.real E_lam :=    measureReal_mono hU_sub_E_lam hE_lam_fin  calc volume.real E_lam_A      = volume.real (E_lam_A ∩ U) + volume.real (E_lam_A \ U) := hE_lam_A_split    _ ≤ 1 / 2 * volume.real U + volume.real (E_lam \ U) := by        linarith [hA_inter_U, hAdiffU_le]    _ = 1 / 2 * volume.real U + (volume.real E_lam - volume.real U) := by        rw [hE_lam_diff]    _ = volume.real E_lam - 1 / 2 * volume.real U := by ring    _ ≤ volume.real E_lam - 1 / 2 * (1 / (5 : ℝ) ^ d * volume.real E_lam) := by        linarith [hU_lower]    _ = (1 - 1 / (2 * 5 ^ d)) * volume.real E_lam := by ring