tree_count

lemma tree_count :    stackSize (𝔘₁ k n j) x ≤ (2 : ℝ) ^ (9 * a - j : ℤ) * stackSize (𝔐 k n) x := by  classical  -- When calculating the LHS, we need only sum over those `u` for which `x ∈ 𝓘 u`.  have : ∑ u ∈ univ.filter (· ∈ 𝔘₁ (X := X) k n j), (𝓘 u : Set X).indicator (1 : X → ℝ) x =      ∑ u ∈ (𝔘₁ k n j).toFinset.filter (x ∈ 𝓘 ·), (𝓘 u : Set X).indicator (1 : X → ℝ) x := by    rw [filter_mem_univ_eq_toFinset (𝔘₁ k n j), sum_filter]    exact sum_congr rfl <|      fun u _ ↦ by simp [Membership.mem]  rw [stackSize_real, this]  -- Use inequality (5.2.20) to bound the LHS by a double sum, then interchange the sums.  apply le_trans (sum_le_sum indicator_le)  simp_rw [← mul_sum, stackSize_real, mem_coe, filter_univ_mem, interchange, sum_const]  let _ : PosMulReflectLE ℝ := inferInstance -- perf: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/performance.20example.20with.20type-class.20inference  -- Replace the cardinality of `𝔘` with the upper bound proven in `card_𝔘m_le`, and simplify.  apply le_of_le_of_eq <| (mul_le_mul_iff_right₀ (zpow_pos two_pos _)).mpr <| sum_le_sum <|    fun _ _ ↦ smul_le_smul_of_nonneg_right card_𝔘m_le <| Set.indicator_apply_nonneg (by simp)  simp_rw [← smul_sum, nsmul_eq_mul, ← mul_assoc, filter_mem_univ_eq_toFinset (𝔐 k n), defaultA]  rw [sub_eq_add_neg, zpow_add₀ two_ne_zero, ← pow_mul, mul_comm 9, mul_comm (2 ^ _)]  norm_cast