Uncertainty

lemma uncertainty' (ha : 1 ≤ a) {p₁ p₂ : 𝔓 X} (hle : 𝔰 p₁ ≤ 𝔰 p₂)    (hinter : (ball (𝔠 p₁) (5 * D ^ 𝔰 p₁) ∩ ball (𝔠 p₂) (5 * D ^ 𝔰 p₂)).Nonempty) {x₁ x₂ : X}    (hx₁ : x₁ ∈ E p₁) (hx₂ : x₂ ∈ E p₂) :    1 + dist_(p₁) (𝒬 p₁) (𝒬 p₂) ≤ C6_2_3 a * (1 + dist_{x₁, D ^ 𝔰 p₁} (Q x₁) (Q x₂)) := by  -- Inequalities 6.2.16.  have hp₁ : dist_(p₁) (𝒬 p₁) (Q x₁) < 1 := by rw [dist_comm]; exact ineq_6_2_16 hx₁  have hp₂ := ineq_6_2_16 hx₂  --Needed for ineq. 6.2.17  have hss : ↑(𝓘 p₁) ⊆ ball (𝔠 p₂) (14 * D^𝔰 p₂) := by    have h1D : 1 ≤ (D : ℝ) := one_le_realD a    have hdist : dist (𝔠 p₁) (𝔠 p₂) < 10 * D ^ 𝔰 p₂ := by      have h5 : 10 * (D : ℝ) ^ 𝔰 p₂ = 5 * D ^ 𝔰 p₂ + 5 * D ^ 𝔰 p₂ := by ring      obtain ⟨y, hy₁, hy₂⟩ := hinter      rw [mem_ball, dist_comm] at hy₁      apply (dist_triangle ..).trans_lt      apply (add_lt_add hy₁ hy₂).trans_le      rw [h5]      gcongr -- uses h1D    refine Grid_subset_ball.trans fun x hx ↦ ?_    rw [mem_ball] at hx ⊢    calc      _ ≤ dist x (𝔠 p₁) + dist (𝔠 p₁) (𝔠 p₂) := dist_triangle ..      _ < 4 * D ^ 𝔰 p₁ + 10 * D ^ 𝔰 p₂ := add_lt_add hx hdist      _ ≤ 4 * D ^ 𝔰 p₂ + 10 * D ^ 𝔰 p₂ := by gcongr -- uses h1D, hle      _ = _ := by ring  -- Inequality 6.2.17.  have hp₁p₂ : dist_(p₁) (Q x₂) (𝒬 p₂) ≤ 2 ^ (6 * a) := by    calc      _ ≤ 2 ^ (6 * a) * dist_(p₂) (Q x₂) (𝒬 p₂) := by        set r := (D : ℝ) ^ 𝔰 p₂ / 4 with hr_def        have hr : 0 < (D : ℝ) ^ 𝔰 p₂ / 4 := by          rw [div_pos_iff_of_pos_right (by positivity)]          exact defaultD_pow_pos a (𝔰 p₂)        have haux : dist_{𝔠 p₂, 2 ^ 6 * r} (Q x₂) (𝒬 p₂) ≤          2 ^ (6 * a) * dist_{𝔠 p₂, r} (Q x₂) (𝒬 p₂) := by          have h6a : (2 : ℝ) ^ (6 * a) = defaultA a ^ 6 := by simp; ring          convert cdist_le_iterate hr (Q x₂) (𝒬 p₂) 6        exact (cdist_mono (ball_subset_Grid.trans          (hss.trans (ball_subset_ball (by linarith))))).trans haux      _ ≤ _ := by        nth_rw 2 [← mul_one (2 ^ _)]        exact mul_le_mul_of_nonneg_left hp₂.le (by positivity)  -- Auxiliary ineq. for 6.2.18  have haux : dist_(p₁) (𝒬 p₁) (𝒬 p₂) ≤ 1 + 2 ^ (6 * a) + dist_(p₁) (Q x₁) (Q x₂) :=    calc      _ ≤ dist_(p₁) (𝒬 p₁) (Q x₁) + dist_(p₁) (Q x₁) (Q x₂) + dist_(p₁) (Q x₂) (𝒬 p₂) :=        dist_triangle4 ..      _ ≤ 1 + dist_(p₁) (Q x₁) (Q x₂) + 2 ^ (6 * a) := add_le_add_three hp₁.le le_rfl hp₁p₂      _ = _ := by ring  calc    -- 6.2.18    _ ≤ 2 + 2 ^ (6 * a) + dist_(p₁) (Q x₁) (Q x₂) := by      have h2 : (2 + 2 ^ (6 * a) : ℝ) = 1 + (1 + 2 ^ (6 * a)) := by ring      rw [h2, add_assoc]      exact add_le_add le_rfl haux    -- 6.2.21    _ ≤ 2 + 2 ^ (6 * a) + dist_{x₁, 8 * D ^ 𝔰 p₁} (Q x₁) (Q x₂) := by      apply add_le_add le_rfl      -- 6.2.19      have h1 : dist (𝔠 p₁) x₁ < 4 * D ^ 𝔰 p₁ := by rw [dist_comm]; exact Grid_subset_ball hx₁.1      -- 6.2.20      have hI : ↑(𝓘 p₁) ⊆ ball x₁ (8 * D ^ 𝔰 p₁) := by        refine Grid_subset_ball.trans fun x hx ↦ ?_        calc          _ ≤ dist x (𝔠 p₁) + dist (𝔠 p₁) x₁ := dist_triangle _ _ _          _ < 4 * D ^ 𝔰 p₁ + 4 * D ^ 𝔰 p₁ := add_lt_add hx h1          _ = _ := by ring      exact cdist_mono (subset_trans ball_subset_Grid hI)    -- 6.2.22    _ ≤ 2 + 2 ^ (6 * a) + 2 ^ (3 * a) * dist_{x₁, D ^ 𝔰 p₁} (Q x₁) (Q x₂) := by      gcongr      have hr : 0 < (D : ℝ) ^ 𝔰 p₁ := defaultD_pow_pos a (𝔰 p₁)      have h8 : (8 : ℝ) = 2 ^ 3 := by norm_num      have h3a : (2 : ℝ) ^ (3 * a) = defaultA a ^ 3 := by simp; ring      convert! cdist_le_iterate hr (Q x₁) (Q x₂) 3 -- uses h8, h3a    -- 6.2.15    _ ≤ _ := by      have hpow : (2 : ℝ) + 2 ^ (6 * a) ≤ 2 ^ (a * 8) :=        calc          _ ≤ (2 : ℝ) ^ (6 * a) + 2 ^ (6 * a) := by            apply add_le_add_left            norm_cast            nth_rw 1 [← pow_one 2]            exact Nat.pow_le_pow_right zero_lt_two (by lia)          _ = 2 * (2 : ℝ) ^ (6 * a) := by ring          _ ≤ _ := by            nth_rw 1 [← pow_one 2, ← pow_add]            norm_cast            exact Nat.pow_le_pow_right zero_lt_two (by lia)      have h38 : 3 ≤ 8 := by lia      have h12 : (1 : ℝ) ≤ 2 := by norm_num      rw [C6_2_3]      conv_rhs => ring_nf      push_cast      rw [mul_comm 3]      gcongr