Drc

lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ ∧ x ∈ A - A ∧ x ∈ f.support)    (hB : (B₁ ∩ B₂).Nonempty) (hA : A.Nonempty) :    ∃ A₁, A₁ ⊆ B₁ ∧ ∃ A₂, A₂ ⊆ B₂ ∧      ⟪μ_[ℝ] A₁ ○ᵈ μ A₂, (↑) ∘ f⟫_[ℝ] * ‖𝟭_[A, ℝ] ○ᵈ 𝟭_[A]‖_[p, μ B₁ ○ᵈ μ B₂] ^ p        ≤ 2 * ∑ x, (μ B₁ ○ᵈ μ B₂) x * (𝟭_[A, ℝ] ○ᵈ 𝟭_[A]) x ^ p * f x ∧      (4 : ℝ) ⁻¹ * ‖𝟭_[A, ℝ] ○ᵈ 𝟭_[A]‖_[p, μ B₁ ○ᵈ μ B₂] ^ (2 * p) / #A ^ (2 * p)        ≤ #A₁ / #B₁ ∧      (4 : ℝ) ⁻¹ * ‖𝟭_[A, ℝ] ○ᵈ 𝟭_[A]‖_[p, μ B₁ ○ᵈ μ B₂] ^ (2 * p) / #A ^ (2 * p)        ≤ #A₂ / #B₂ := by  have := hB.mono inter_subset_left  have := hB.mono inter_subset_right  have hp₀ : p ≠ 0 := by positivity  have := dLpNorm_ddconv_pos hp₀ hB hA  set M : ℝ :=    2 ⁻¹ * ‖𝟭_[A, ℝ] ○ᵈ 𝟭_[A]‖_[p, μ B₁ ○ᵈ μ B₂] ^ p * (sqrt #B₁ * sqrt #B₂) / #A ^ p      with hM_def  have hM : 0 < M := by rw [hM_def]; positivity  replace hf : 0 < ∑ x, (μ_[ℝ] B₁ ○ᵈ μ B₂) x * (𝟭_[A] ○ᵈ 𝟭_[A]) x ^ p * f x := by    have : 0 ≤ μ_[ℝ] B₁ ○ᵈ μ B₂ * (𝟭_[A] ○ᵈ 𝟭_[A]) ^ p * (↑) ∘ f := -- positivity      mul_nonneg (mul_nonneg (dddconv_nonneg mu_nonneg mu_nonneg) <| pow_nonneg        (dddconv_nonneg Set.indicator_one_nonneg Set.indicator_one_nonneg) _) fun _ ↦ by simp    refine Fintype.sum_pos <| this.lt_iff_ne'.2 <| support_nonempty_iff.1 ?_    simp only [support_comp_eq, Set.Nonempty, and_assoc, support_mul', support_dddconv,      Set.indicator_one_nonneg, mu_nonneg, Set.support_indicator_one, support_mu,      NNReal.coe_eq_zero,iff_self, forall_const, Set.mem_inter_iff, ← coe_sub, mem_coe,      support_pow' _ hp₀, hf]  set A₁ := fun s ↦ B₁ ∩ c p A s  set A₂ := fun s ↦ B₂ ∩ c p A s  set g : (Fin p → G) → ℝ := fun s ↦ #(A₁ s) * #(A₂ s) with hg_def  have hg : ∀ s, 0 ≤ g s := fun s ↦ by rw [hg_def]; dsimp; positivity  have hgB : ∑ s, g s = #B₁ * #B₂ * ‖𝟭_[A, ℝ] ○ᵈ 𝟭_[A]‖_[p, μ B₁ ○ᵈ μ B₂] ^ p := by    have hAdddconv : 0 ≤ 𝟭_[(A : Set G), ℝ] ○ᵈ 𝟭_[A] :=      dddconv_nonneg Set.indicator_one_nonneg Set.indicator_one_nonneg    simpa only [wLpNorm_pow_eq_sum_norm hp₀, norm_of_nonneg (hAdddconv _), NNReal.smul_def,      NNReal.coe_dddconv, NNReal.coe_comp_mu, wInner_one_eq_sum, Pi.one_apply, inner_apply',      ← coe_inter, conj_to_real, mul_one, sum_dddconv, sum_indicator_one, nsmul_eq_mul,      Nat.cast_mul, g, A₁, A₂] using! lemma_0 p B₁ B₂ A 1  suffices ∑ s, ⟪𝟭_[A₁ s, ℝ] ○ᵈ 𝟭_[A₂ s], (↑) ∘ f⟫_[ℝ] * ‖𝟭_[A, ℝ] ○ᵈ 𝟭_[A]‖_[p, μ B₁ ○ᵈ μ B₂] ^ p    < ∑ s, 𝟭_[({s | M ^ 2 ≤ g s} : Finset _)] s * g s *        (2 * ∑ x, (μ B₁ ○ᵈ μ B₂) x * (𝟭_[A, ℝ] ○ᵈ 𝟭_[A]) x ^ p * f x) by    obtain ⟨s, -, hs⟩ := exists_lt_of_sum_lt this    refine ⟨_, inter_subset_left (s₂ := c p A s), _, inter_subset_left (s₂ := c p A s), ?_⟩    simp only [Set.indicator_apply, boole_mul] at hs    split_ifs at hs with h; swap    · simp only [zero_mul, wInner_one_eq_sum, Function.comp_apply, RCLike.inner_apply',        RCLike.conj_to_real] at hs      have : 0 ≤ 𝟭_[(A₁ s : Set G), ℝ] ○ᵈ 𝟭_[A₂ s] :=        dddconv_nonneg Set.indicator_one_nonneg Set.indicator_one_nonneg      -- positivity      cases hs.not_ge <|        mul_nonneg (sum_nonneg fun x _ ↦ mul_nonneg (this _) <| by positivity) <| by positivity    have : (4 : ℝ) ⁻¹ * ‖𝟭_[A, ℝ] ○ᵈ 𝟭_[A]‖_[p, μ B₁ ○ᵈ μ B₂] ^ (2 * p) / #A ^ (2 * p)      ≤ #(A₁ s) / #B₁ * (#(A₂ s) / #B₂) := by      rw [div_mul_div_comm, le_div_iff₀ (by positivity)]      simpa [hg_def, hM_def, mul_pow, div_pow, pow_mul', show (2 : ℝ) ^ 2 = 4 by norm_num,        mul_div_right_comm] using h    refine ⟨(lt_of_mul_lt_mul_left (hs.trans_eq' ?_) <| hg s).le, this.trans <|      mul_le_of_le_one_right ?_ <| div_le_one_of_le₀ ?_ ?_, this.trans <|      mul_le_of_le_one_left ?_ <| div_le_one_of_le₀ ?_ ?_⟩    · simp_rw [A₁, A₂, g, ← card_smul_mu, smul_dddconv, dddconv_smul, ← Nat.cast_smul_eq_nsmul ℝ,        wInner_smul_left, smul_eq_mul, star_trivial, mul_assoc, A₁, A₂]    any_goals positivity    all_goals exact Nat.cast_le.2 <| card_mono inter_subset_left  rw [← sum_mul, lemma_0, nsmul_eq_mul, Nat.cast_mul, ← sum_mul, mul_right_comm, ← hgB,    mul_left_comm, ← mul_assoc]  simp only [Set.indicator_apply, boole_mul, mem_coe, mem_filter, mem_univ, true_and, ← sum_filter,    mul_lt_mul_iff_left₀ hf, Function.comp_apply]  by_cases h : ∀ s, g s ≠ 0 → M ^ 2 ≤ g s  · rw [← sum_filter_ne_zero (s := filter _ _), Finset.filter_comm,      filter_true_of_mem fun s hs ↦ h s (mem_filter.1 hs).2, ← sum_filter_ne_zero]    refine lt_mul_of_one_lt_left (sum_pos (fun s hs ↦ (h _ (mem_filter.1 hs).2).trans_lt' <|      by positivity) ?_) one_lt_two    rw [← sum_filter_ne_zero] at hgB    exact nonempty_of_sum_ne_zero <| hgB.trans_ne <| by positivity  push Not at h  obtain ⟨s, hs⟩ := h  suffices h : (2 : ℝ) * ∑ s with g s < M ^ 2, g s < ∑ s, g s by    refine (le_or_lt_of_add_le_add ?_).resolve_left h.not_ge    simp_rw [← not_le, ← compl_filter, ← two_mul, ← mul_add, sum_compl_add_sum]    rfl  rw [← lt_div_iff₀' (zero_lt_two' ℝ), div_eq_inv_mul]  calc    ∑ s with g s < M ^ 2, g s = ∑ s with g s < M ^ 2 ∧ g s ≠ 0, sqrt (g s) * sqrt (g s)          := by simp_rw [mul_self_sqrt (hg _), ← filter_filter, sum_filter_ne_zero]    _ < ∑ s with g s < M ^ 2 ∧ g s ≠ 0, M * sqrt (g s)        := sum_lt_sum_of_nonempty ⟨s, mem_filter.2 ⟨mem_univ _, hs.symm⟩⟩ ?_    _ ≤ ∑ s, M * sqrt (g s) := sum_le_univ_sum_of_nonneg fun s ↦ by positivity    _ = M * (∑ s, sqrt #(A₁ s) * sqrt #(A₂ s))        := by simp_rw [mul_sum, g, sqrt_mul <| Nat.cast_nonneg _]    _ ≤ M * (sqrt (∑ s, #(A₁ s)) * sqrt (∑ s, #(A₂ s))) := by      gcongr; exact sum_sqrt_mul_sqrt_le _ fun i ↦ by positivity fun i ↦ by positivity    _ = _ := ?_  · simp only [mem_filter, mem_univ, true_and, and_imp]    exact fun s hsM hs ↦ mul_lt_mul_of_pos_right ((sqrt_lt' hM).2 hsM) <|      sqrt_pos.2 <| (hg _).lt_of_ne' hs  rw [sum_cast_c, sum_cast_c, sqrt_mul', sqrt_mul', mul_mul_mul_comm (sqrt _), mul_self_sqrt,    ← mul_assoc, hM_def, div_mul_cancel₀, ← sqrt_mul, mul_assoc, mul_self_sqrt, hgB, mul_right_comm,    mul_assoc]  all_goals positivity