dach_bound

lemma dach_bound (h𝔄 : IsAntichain (· ≤ ·) 𝔄) {p : 𝔓 X} (mp : p ∈ 𝔄) (hg : Measurable g)    (hgG : ∀ x, ‖g x‖ ≤ G.indicator 1 x) {x₀ : X} (hx : x₀ ∈ ball (𝔠 p) (14 * D ^ 𝔰 p)) :    dach 𝔄 p g ≤ C6_1_6 a * dens₁ 𝔄 ^ (p₆ a : ℝ)⁻¹ * M14 𝔄 (q₆ a) g x₀ := by  classical  unfold dach  set B := ball (𝔠 p) (14 * D ^ 𝔰 p)  set A : Set (𝔓 X) := {p' | (p' ∈ 𝔄 ∧ 𝔰 p' ≤ 𝔰 p) ∧ (𝓘 p' : Set X) ⊆ B}  have sA : A ⊆ 𝔄 := fun _ ↦ by simp only [A, mem_setOf_eq, and_imp]; tauto  calc    _ = (volume B)⁻¹ * ∫⁻ x, B.indicator (‖g ·‖ₑ) x *          ∑ p' with p' ∈ A, (1 + edist_(p') (𝒬 p') (𝒬 p)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) *            (E p').indicator 1 x * G.indicator 1 x := by      congr! with x; change ∑ p' with p' ∈ A, _ = _      rw [Finset.mul_sum]      conv_rhs =>        enter [2, p']        rw [← mul_assoc, ← mul_assoc, mul_comm _ (_ ^ _), mul_assoc, mul_assoc]      congr! 2 with p' mp'      rw [← mul_assoc, ← inter_indicator_mul]; simp_rw [Pi.one_apply, mul_one]      simp_rw [A, mem_setOf_eq, Finset.mem_filter_univ] at mp'      rw [inter_eq_right.mpr (E_subset_𝓘.trans mp'.2)]      by_cases hx : x ∈ G      · rw [indicator_of_mem hx, Pi.one_apply, mul_one]      · specialize hgG x; rw [indicator_of_notMem hx, norm_le_zero_iff] at hgG        have : (E p').indicator (‖g ·‖ₑ) x = 0 := by          rw [indicator_apply_eq_zero, hgG, enorm_zero]; exact fun _ ↦ rfl        rw [this, zero_mul]    _ ≤ (volume B)⁻¹ * eLpNorm (B.indicator (‖g ·‖ₑ)) (ENNReal.ofReal (q₆ a)) *        eLpNorm (fun x ↦ ∑ p' with p' ∈ A,          (1 + edist_(p') (𝒬 p') (𝒬 p)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) *          (E p').indicator 1 x * G.indicator 1 x) (ENNReal.ofReal (p₆ a)) := by      rw [mul_assoc]; gcongr; apply lintegral_mul_le_eLpNorm_mul_eLqNorm      · exact Real.HolderConjugate.ennrealOfReal (holderConjugate_p₆ (four_le_a X)).symm      · fun_prop (discharger := measurability)      · refine Finset.aemeasurable_fun_sum _ fun p' mp' ↦ ?_        simp_rw [mul_assoc, ← inter_indicator_mul]        exact (AEMeasurable.indicator (by simp) (measurableSet_E.inter measurableSet_G)).const_mul _    _ ≤ (volume B)⁻¹ * (volume B ^ (q₆ a)⁻¹ * M14 𝔄 (q₆ a) g x₀) *        (C6_1_6 a * dens₁ A ^ (p₆ a)⁻¹ * volume (⋃ t ∈ A, (𝓘 t : Set X)) ^ (p₆ a)⁻¹) := by      gcongr      · exact eLpNorm_le_M14 mp hx (q₆_pos (four_le_a X))      · convert! tile_count (h𝔄.subset sA) ⟨𝒬 p, range_𝒬 (mem_range_self p)⟩    _ ≤ (volume B)⁻¹ * (volume B ^ (q₆ a)⁻¹ * M14 𝔄 (q₆ a) g x₀) *        (C6_1_6 a * dens₁ 𝔄 ^ (p₆ a)⁻¹ * volume B ^ (p₆ a)⁻¹) := by      have : 0 ≤ (p₆ a)⁻¹ := by rw [Right.inv_nonneg]; exact (p₆_pos (four_le_a X)).le      gcongr      · exact dens₁_mono sA      · refine iUnion₂_subset fun p' mp' ↦ ?_        simp_rw [A, mem_setOf_eq] at mp'; exact mp'.2    _ = _ := by      rw [mul_comm, mul_assoc]; congr 1      have vpos : 0 < volume B := by apply measure_ball_pos; unfold defaultD; positivity      rw [← mul_assoc, ← ENNReal.rpow_neg_one, ← ENNReal.rpow_add _ _ vpos.ne' (by finiteness),        ← mul_assoc, ← ENNReal.rpow_add _ _ vpos.ne' (by finiteness),        ← add_rotate, (holderConjugate_p₆ (four_le_a X)).symm.inv_add_inv_eq_one,        add_neg_cancel, ENNReal.rpow_zero, one_mul]