john_nirenberg

lemma john_nirenberg : volume (setA (X := X) l k n) ≤ 2 ^ (k + 1 - l : ℤ) * volume G := by  induction l with  | zero =>    calc      _ ≤ volume (⋃ i ∈ 𝓒 (X := X) k, (i : Set X)) := measure_mono setA_subset_iUnion_𝓒      _ ≤ _ := by        rw [← ENNReal.rpow_intCast, show (k + 1 - (0 : ℕ) : ℤ) = (k + 1 : ℝ) by simp]        exact_mod_cast dense_cover k  | succ l ih =>    suffices 2 * volume (setA (X := X) (l + 1) k n) ≤ volume (setA (X := X) l k n) by      rw [← ENNReal.mul_le_mul_iff_right (a := 2) (by simp) (by simp), ← mul_assoc]      apply this.trans      convert! ih using 2; nth_rw 1 [← zpow_one 2, ← ENNReal.zpow_add (by simp) (by simp)]      congr 1; lia    calc      _ = 2 * ∑ L ∈ Grid.maxCubes (MsetA (X := X) l k n),          volume (setA (X := X) (l + 1) k n ∩ L) := by        congr; rw [← measure_biUnion_finset]        · congr with x; constructor <;> intro h          · obtain ⟨L', mL'⟩ := dyadic_union h            have := mem_of_mem_of_subset mL'.1 (mL'.2.trans setA_subset_setA)            rw [← iUnion_MsetA_eq_setA, mem_iUnion₂] at this            obtain ⟨M, mM, lM⟩ := this            obtain ⟨L, mL, lL⟩ := Grid.exists_maximal_supercube mM            rw [mem_iUnion₂]; use L, mL            exact ⟨mem_of_mem_of_subset mL'.1 mL'.2, mem_of_mem_of_subset lM lL.1⟩          · rw [mem_iUnion₂] at h; obtain ⟨i, _, mi₂⟩ := h; exact mem_of_mem_inter_left mi₂        · exact fun i mi j mj hn ↦            ((Grid.maxCubes_pairwiseDisjoint mi mj hn).inter_left' _).inter_right' _        · exact fun _ _ ↦ measurable_setA.inter coeGrid_measurable      _ ≤ ∑ L ∈ Grid.maxCubes (MsetA (X := X) l k n), volume (L : Set X) := by        rw [Finset.mul_sum]; exact Finset.sum_le_sum fun L mL ↦ john_nirenberg_aux2 mL      _ = _ := by        rw [← measure_biUnion_finset Grid.maxCubes_pairwiseDisjoint (fun _ _ ↦ coeGrid_measurable)]        congr with x; constructor <;> intro h        · rw [mem_iUnion₂] at h; obtain ⟨i, mi₁, mi₂⟩ := h          simp only [Grid.maxCubes, Finset.mem_filter, MsetA, Finset.mem_univ, true_and] at mi₁          exact mem_of_mem_of_subset mi₂ mi₁.1        · obtain ⟨L', mL'⟩ := dyadic_union h          have := mem_of_mem_of_subset mL'.1 mL'.2          rw [← iUnion_MsetA_eq_setA, mem_iUnion₂] at this          obtain ⟨M, mM, lM⟩ := this          obtain ⟨L, mL, lL⟩ := Grid.exists_maximal_supercube mM          rw [mem_iUnion₂]; use L, mL, mem_of_mem_of_subset lM lL.1