john_nirenberg_aux2

lemma john_nirenberg_aux2 {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n)) :    2 * volume (setA (X := X) (l + 1) k n ∩ L) ≤ volume (L : Set X) := by  classical  let Q₁ : Finset (𝔓 X) := { q | q ∈ 𝔐 (X := X) k n ∧ 𝓘 q ≤ L }  have Q₁m : ∀ i ∈ Q₁, Measurable ((𝓘 i : Set X).indicator (1 : X → ℝ≥0∞)) := fun _ _ ↦    measurable_one.indicator coeGrid_measurable  have e528 : ∑ q ∈ Q₁, volume (E₁ q) ≤ volume (L : Set X) :=    calc      _ = volume (⋃ q ∈ Q₁, E₁ q) := by        refine (measure_biUnion_finset (fun p mp q mq hn ↦ ?_) (fun _ _ ↦ ?_)).symm        · simp_rw [Finset.mem_coe, Q₁, Finset.mem_filter] at mp mq          exact pairwiseDisjoint_E1 mp.2.1 mq.2.1 hn        · exact (coeGrid_measurable.inter measurableSet_G).inter            (SimpleFunc.measurableSet_preimage ..)      _ ≤ volume (⋃ q ∈ Q₁, (𝓘 q : Set X)) := measure_mono (iUnion₂_mono fun q _ ↦ E₁_subset q)      _ ≤ _ := by        apply measure_mono (iUnion₂_subset fun q mq ↦ ?_)        simp_rw [Q₁, Finset.mem_filter] at mq; exact mq.2.2.1  have e529 : ∑ q ∈ Q₁, volume (𝓘 q : Set X) ≤ 2 ^ n * volume (L : Set X) :=    calc      _ ≤ ∑ q ∈ Q₁, 2 ^ n * volume (E₁ q) := by        refine Finset.sum_le_sum fun q mq ↦ ?_        simp_rw [Q₁, Finset.mem_filter, 𝔐, mem_setOf, maximal_iff, aux𝔐, mem_setOf] at mq        replace mq := mq.2.1.1.2        rw [← ENNReal.rpow_intCast, show (-(n : ℕ) : ℤ) = (-n : ℝ) by simp, mul_comm,          ← ENNReal.lt_div_iff_mul_lt (by simp) (by simp), ENNReal.div_eq_inv_mul,          ← ENNReal.rpow_neg, neg_neg] at mq        exact_mod_cast mq.le      _ ≤ _ := by rw [← Finset.mul_sum]; exact mul_le_mul_right e528 _  rw [← ENNReal.mul_le_mul_iff_right (a := 2 ^ n) (by simp) (by simp), ← mul_assoc, ← pow_succ]  calc    _ = ∫⁻ x in setA (X := X) (l + 1) k n ∩ L, 2 ^ (n + 1) := (setLIntegral_const _ _).symm    _ ≤ ∫⁻ x in setA (X := X) (l + 1) k n ∩ L, ∑ q ∈ Q₁, (𝓘 q : Set X).indicator 1 x := by      refine setLIntegral_mono (Finset.measurable_sum Q₁ Q₁m) fun x ⟨mx, mx₂⟩ ↦ ?_      have : 2 ^ (n + 1) ≤ ∑ q ∈ Q₁, (𝓘 q : Set X).indicator 1 x := by        convert john_nirenberg_aux1 mL mx mx₂        simp_rw [stackSize, Q₁, mem_setOf_eq]      have lcast : (2 : ℝ≥0∞) ^ (n + 1) = ((2 ^ (n + 1) : ℕ) : ℝ).toNNReal := by        rw [Real.toNNReal_natCast, ENNReal.coe_natCast]; norm_cast      have rcast : ∑ q ∈ Q₁, (𝓘 q : Set X).indicator (1 : X → ℝ≥0∞) x =          (((∑ q ∈ Q₁, (𝓘 q : Set X).indicator (1 : X → ℕ) x) : ℕ) : ℝ).toNNReal := by        rw [Real.toNNReal_natCast, ENNReal.coe_natCast, Nat.cast_sum]; congr!; simp [indicator]      rw [lcast, rcast, ENNReal.coe_le_coe]      exact Real.toNNReal_le_toNNReal (Nat.cast_le.mpr this)    _ ≤ ∫⁻ x, ∑ q ∈ Q₁, (𝓘 q : Set X).indicator 1 x := setLIntegral_le_lintegral _ _    _ = ∑ q ∈ Q₁, ∫⁻ x, (𝓘 q : Set X).indicator 1 x := lintegral_finsetSum _ Q₁m    _ = ∑ q ∈ Q₁, volume (𝓘 q : Set X) := by      congr!; exact lintegral_indicator_one coeGrid_measurable    _ ≤ _ := e529