Sifting cor

lemma sifting_cor (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even p) (hp₀ : p ≠ 0)    (hpε : ε⁻¹ * log (2 / δ) ≤ p) (hA : A.Nonempty) :    ∃ A₁ A₂, 1 - δ ≤ ∑ x ∈ s p ε univ univ A, (μ A₁ ○ᵈ μ A₂) x ∧        (4 : ℝ)⁻¹ * A.dens ^ (2 * p) ≤ A₁.dens ∧          (4 : ℝ)⁻¹ * A.dens ^ (2 * p) ≤ A₂.dens := by  by_cases hf :      ∃ x, x ∈ A - A ∧ (𝟭_[A] ○ᵈ 𝟭_[A]) x ≤ (1 - ε) * ‖𝟭_[(A : Set G), ℝ] ○ᵈ 𝟭_[A]‖_[p, μ univ]  · have hp₀ : p ≠ 0 := by positivity    have :      (4 : ℝ)⁻¹ * A.dens ^ (2 * p) ≤        4⁻¹ * ‖𝟭_[(A : Set G), ℝ] ○ᵈ 𝟭_[A]‖_[p, μ univ] ^ (2 * p) / #A ^ (2 * p) := by      rw [mul_div_assoc, ← div_pow]      gcongr      rw [nnratCast_dens, le_div_iff₀ (by positivity), ← mul_div_right_comm]      have : Nonempty G := ⟨hA.choose⟩      have hμ_univ : ∑ x : G, ((μ univ x : ℝ≥0) : ℝ≥0∞) = 1 := mod_cast sum_mu ℝ≥0 univ_nonempty      calc        _ = (‖𝟭_[(A : Set G), ℝ] ○ᵈ 𝟭_[A]‖_[1, μ univ] : ℝ) := by          simp [mu, wLpNorm_smul_right, dL1Norm_dddconv, card_univ, inv_mul_eq_div]        _ ≤ _ := wLpNorm_mono_right hμ_univ          (one_le_two.trans <| by obtain ⟨k, rfl⟩ := hp; norm_cast; lia) _    obtain ⟨A₁, -, A₂, -, h, hcard₁, hcard₂⟩ :=      sifting univ univ hε hε₁ hδ hp (by obtain ⟨k, rfl⟩ := hp; lia) hpε (by simp) hA (by simpa)    exact ⟨A₁, A₂, h, this.trans <| by simpa [nnratCast_dens] using hcard₁,      this.trans <| by simpa [nnratCast_dens] using hcard₂⟩  · refine ⟨A, A, ?_, ?_⟩    · rw [Fintype.sum_subset]      · simpa [sum_dddconv, sum_mu, hA] using hδ.le      · simpa [← Function.mem_support, ← coe_sub] using hf    · rw [and_self]      calc        (4 : ℝ)⁻¹ * A.dens ^ (2 * p) ≤ 1 * A.dens ^ 1 := by          gcongr ?_ * ?_          · norm_num          · exact pow_le_pow_of_le_one (by positivity) (mod_cast A.dens_le_one) (by omega)        _ = A.dens := by simp