From fdf917b00b203544eb08848167bf1f0164e9f884 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 21 Oct 2026 02:58:39 +0000 Subject: [PATCH] Reduce QuantumQuery proof elaboration cost --- LeanPool/QuantumQuery/Adversary.lean | 56 +++++++++---------- LeanPool/QuantumQuery/Algorithms.lean | 14 ++--- LeanPool/QuantumQuery/QueryBounds.lean | 16 +++--- LeanPool/QuantumQuery/StateConversion.lean | 63 ++++++++++++---------- 4 files changed, 75 insertions(+), 74 deletions(-) diff --git a/LeanPool/QuantumQuery/Adversary.lean b/LeanPool/QuantumQuery/Adversary.lean index 5a3cf489d2..491d6369b2 100644 --- a/LeanPool/QuantumQuery/Adversary.lean +++ b/LeanPool/QuantumQuery/Adversary.lean @@ -297,7 +297,7 @@ lemma abs_apply_le_sqrt_dotProduct_self (x : n → ℝ) (i : n) : lemma dotProduct_mulVec_eq_sum (A : Matrix n n ℝ) (u w : n → ℝ) : u ⬝ᵥ A *ᵥ w = ∑ x, ∑ y, u x * A x y * w y := by - simp [dotProduct, Matrix.mulVec, Finset.mul_sum, mul_assoc] + simp only [dotProduct, Matrix.mulVec, Finset.mul_sum, mul_assoc] variable [DecidableEq n] @@ -345,7 +345,8 @@ theorem l2_opNorm_le_of_forall_dotProduct (A : Matrix n n ℝ) {c : ℝ} · rw [← h0] positivity · rw [habs, hww] at key - nlinarith [key, h0, Real.sqrt_nonneg (y ⬝ᵥ y)] + rw [mul_right_comm c s] at key + exact (mul_le_mul_iff_left₀ h0).mp key /-- Every entry is bounded by the L2 operator norm. -/ theorem abs_entry_le_l2_opNorm (A : Matrix n n ℝ) (x y : n) : |A x y| ≤ ‖A‖ := by @@ -595,7 +596,7 @@ lemma norm_le_of_feasible (h1 : IsAdvMatrix f Γ) Finset.sum_le_sum fun x _ => Finset.sum_le_sum fun y _ => abs_apply_le_one_of_feasible h1 h2 x y _ = (Fintype.card (ι → σ) : ℝ) ^ 2 := by - simp [Finset.sum_const, Finset.card_univ, pow_two] + simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one, pow_two] lemma bddAbove_advPM_set (f : (ι → σ) → O) : BddAbove {r : ℝ | ∃ Γ, IsAdvMatrix f Γ ∧ (∀ i, ‖Γ ⊙ advD i‖ ≤ 1) ∧ @@ -681,9 +682,7 @@ lemma pairMatrix_isHermitian (x y : ι → σ) : lemma single_one_mulVec (a b : ι → σ) (u : (ι → σ) → ℝ) : Matrix.single a b (1 : ℝ) *ᵥ u = fun w => if a = w then u b else 0 := by funext w - by_cases haw : a = w - · simp [Matrix.mulVec, dotProduct, Matrix.single_apply, haw] - · simp [Matrix.mulVec, dotProduct, haw] + simp only [Matrix.single_mulVec, one_mul, Function.update_apply, Pi.zero_apply, eq_comm] lemma pairMatrix_mulVec (x y : ι → σ) (u : (ι → σ) → ℝ) : pairMatrix x y *ᵥ u @@ -919,13 +918,12 @@ lemma mulVec_brestrict {M : Matrix U U ℝ} {χ : U → Bool} by_cases hv : χ v = b · rw [ite_eq_left hv, hM u v (hu.trans hv.symm), zero_mul] · rw [ite_eq_right hv] - · have hu' : χ u = !b := by cases hcu : χ u <;> cases b <;> simp_all + · have hu' : χ u = !b := Bool.eq_not_of_ne hu rw [ite_eq_left hu'] refine Finset.sum_congr rfl fun v _ => ?_ by_cases hv : χ v = b · rw [ite_eq_left hv] - · have hv' : χ v = χ u := by - cases hcv : χ v <;> cases hcu : χ u <;> cases b <;> simp_all + · have hv' : χ v = χ u := (Bool.eq_not_of_ne hv).trans hu'.symm rw [ite_eq_right hv, hM u v hv'.symm, zero_mul] lemma mulVec_brestrict_eigen {M : Matrix U U ℝ} {χ : U → Bool} @@ -3064,8 +3062,8 @@ lemma hat_guarded_row_sumGen {g : (Y) → Bool} by_cases h : g u = b · rw [ite_eq_left h] · rw [ite_eq_right h] - have hgg : g u = g u₀ := by - cases hgu : g u <;> cases hgu0 : g u₀ <;> cases b <;> simp_all + have hgg : g u = g u₀ := + (Bool.eq_not_of_ne h).trans (Bool.eq_not_of_ne h0).symm rw [hN.apply_eq_zero hgg.symm, zero_mul] rw [Finset.sum_congr rfl fun u _ => hall u] have hcf := congrFun hv u₀ @@ -3901,7 +3899,7 @@ lemma norm_le_of_feasibleOn (hdet : ∀ x y, read x = read y → f x = f y) Finset.sum_le_sum fun x _ => Finset.sum_le_sum fun y _ => abs_apply_le_one_of_feasibleOn hdet h1 h2 x y _ = (Fintype.card X : ℝ) ^ 2 := by - simp [Finset.sum_const, Finset.card_univ, pow_two] + simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one, pow_two] omit [DecidableEq ι] [Fintype ι] in lemma bddAbove_advPMOn_set (hdet : ∀ x y, read x = read y → f x = f y) : @@ -4684,7 +4682,7 @@ theorem lt_advPMOn_of_certificate {read : X → ι → σ} {f : X → Bool} l2_opNorm_hadamard_dualTargetOn_le f _ have h2 : ‖(2 : ℝ)⁻¹‖ = (2 : ℝ)⁻¹ := by norm_num rw [h2] - nlinarith [hnorm i, norm_nonneg ((Γ' ⊙ advDOn read i) ⊙ dualTargetOn f)] + linarith only [h1, hnorm i] set R := Real.sqrt (∑ x, p x) with hR have hR0 : 0 < R := Real.sqrt_pos.mpr hsum have hRR : R * R = ∑ x, p x := Real.mul_self_sqrt hsum.le @@ -4713,7 +4711,7 @@ theorem lt_advPMOn_of_certificate {read : X → ι → σ} {f : X → Bool} field_simp have hlt : c < a ⬝ᵥ Γ'' *ᵥ a := by rw [hval, lt_div_iff₀ (by positivity)] - linarith [hobj] + linarith only [hobj] have hbound : a ⬝ᵥ Γ'' *ᵥ a ≤ ‖Γ''‖ := by have := abs_dotProduct_mulVec_le Γ'' a a rw [haa, Real.sqrt_one] at this @@ -5245,7 +5243,7 @@ theorem exists_dualPairOn_of_advPMOn_lt {read : X → ι → σ} {f : X → Bool have hexp : κ * ((∑ x, s x * s x) + ∑ x, t x * t x) = κ * (∑ x, s x * s x) + κ * (∑ x, t x * t x) := by ring rw [hexp] at h - linarith + linarith only [h] have hquadabs : ∀ (i : ι) (s t : X → ℝ), |s ⬝ᵥ (Ξ ⊙ advDOn read i) *ᵥ t| ≤ (∑ x, P false x * (s x * s x)) + ∑ x, P true x * (t x * t x) := by @@ -5261,7 +5259,7 @@ theorem exists_dualPairOn_of_advPMOn_lt {read : X → ι → σ} {f : X → Bool = ∑ x, P false x * (s x * s x) := Finset.sum_congr rfl fun x _ => by ring rw [hneg, hsq] at h2 - exact abs_le.mpr ⟨by linarith, by linarith⟩ + exact abs_le.mpr ⟨by linarith only [h2], h1⟩ -- the weights are strictly positive have hsingle_ne : ∀ x : X, (Pi.single x (1 : ℝ) : X → ℝ) ≠ 0 := by intro x h @@ -5279,7 +5277,7 @@ theorem exists_dualPairOn_of_advPMOn_lt {read : X → ι → σ} {f : X → Bool simp only [Pi.zero_apply, mul_zero, Finset.sum_const_zero, add_zero, hz, zero_add] at h rw [hP] - linarith + linarith only [h] | true => have h := hQbound (concVecOn i₀ 0 (Pi.single x 1)) (concVecOn_ne_zero_right (hsingle_ne x)) @@ -5289,7 +5287,7 @@ theorem exists_dualPairOn_of_advPMOn_lt {read : X → ι → σ} {f : X → Bool simp only [Pi.zero_apply, mul_zero, Finset.sum_const_zero, zero_add, hz] at h rw [hP] - linarith + linarith only [h] -- the objective hypothesis of the certificate have hcorner := hbox _ (dualCornerOn_mem (f := f) hc0.le) have hcornerval : φ (dualCornerOn f c) @@ -5322,7 +5320,7 @@ theorem exists_dualPairOn_of_advPMOn_lt {read : X → ι → σ} {f : X → Bool rw [← hkappa, hTdef] ring rw [hLHS] - linarith + linarith only [hcorner, huv] exact absurd (lt_advPMOn_of_certificate_two hdet (hPpos false) (hPpos true) hquadabs hobj) (not_lt.mpr hc.le) @@ -6810,8 +6808,9 @@ lemma sqrt_card_le_norm_starMatrix {S : Finset (ι → σ)} {c : ι → σ} ring have h2k : Real.sqrt (2 * k) * Real.sqrt (2 * k) = 2 * k := Real.mul_self_sqrt (by positivity) - rw [habs] at h - nlinarith [h, h2k, hkpos, Real.sqrt_nonneg k] + rw [habs, mul_assoc ‖starMatrix S c‖, h2k, + mul_comm ‖starMatrix S c‖ (2 * k)] at h + exact le_of_mul_le_mul_left h (mul_pos (by norm_num) hkpos) theorem norm_starMatrix {S : Finset (ι → σ)} {c : ι → σ} (hc : c ∉ S) (hS : S.Nonempty) : ‖starMatrix S c‖ = Real.sqrt (S.card : ℝ) := @@ -6994,8 +6993,9 @@ lemma sqrt_starWeight_le_norm_wStarMatrix {S : Finset (ι → σ)} ring have h2W : Real.sqrt (2 * W) * Real.sqrt (2 * W) = 2 * W := Real.mul_self_sqrt (by positivity) - rw [habs] at h - nlinarith [h, h2W, hW, Real.sqrt_nonneg W] + rw [habs, mul_assoc ‖wStarMatrix S c w‖, h2W, + mul_comm ‖wStarMatrix S c w‖ (2 * W)] at h + exact le_of_mul_le_mul_left h (mul_pos (by norm_num) hW) theorem norm_wStarMatrix {S : Finset (ι → σ)} {c : ι → σ} (hc : c ∉ S) {w : (ι → σ) → ℝ} (hW : 0 < starWeight S w) : @@ -7308,10 +7308,7 @@ noncomputable def orNDual [Nonempty ι] : DualPair Unit (orN : (ι → Bool) → omit [DecidableEq ι] in lemma orNDual_isCostLe [Nonempty ι] : (orNDual (ι := ι)).IsCostLe (Real.sqrt (Fintype.card ι : ℝ)) := by - have hδ : orNDelta ι ≠ 0 := orNDelta_ne_zero have hn : (0:ℝ) < (Fintype.card ι : ℝ) := by exact_mod_cast Fintype.card_pos - have hs : Real.sqrt (Fintype.card ι : ℝ) * Real.sqrt (Fintype.card ι : ℝ) - = (Fintype.card ι : ℝ) := Real.mul_self_sqrt hn.le have key : ∀ x : ι → Bool, (∑ i : ι, ∑ _k : Unit, orNDualVec x i * orNDualVec x i) ≤ Real.sqrt (Fintype.card ι : ℝ) := by @@ -7347,16 +7344,13 @@ lemma orNDual_isCostLe [Nonempty ι] : ((1 / ((supportCard x : ℝ) * orNDelta ι)) * (1 / ((supportCard x : ℝ) * orNDelta ι))) = Real.sqrt (Fintype.card ι : ℝ) / (supportCard x : ℝ) := by - rw [orNDelta] at * + rw [div_mul_div_comm, one_mul, mul_mul_mul_comm, orNDelta_sq] field_simp - nlinarith [hs, Real.sq_sqrt (Real.sqrt_nonneg (Fintype.card ι : ℝ)), - Real.sqrt_nonneg (Fintype.card ι : ℝ), - Real.mul_self_sqrt (Real.sqrt_nonneg (Fintype.card ι : ℝ))] rw [hval] have hone : (1:ℝ) ≤ (supportCard x : ℝ) := by exact_mod_cast supportCard_pos hx rw [div_le_iff₀ hpos] - nlinarith [Real.sqrt_nonneg (Fintype.card ι : ℝ), hone] + exact le_mul_of_one_le_right (Real.sqrt_nonneg _) hone exact ⟨key, key⟩ omit [DecidableEq ι] in diff --git a/LeanPool/QuantumQuery/Algorithms.lean b/LeanPool/QuantumQuery/Algorithms.lean index 4d29abff6e..acb176f9bb 100644 --- a/LeanPool/QuantumQuery/Algorithms.lean +++ b/LeanPool/QuantumQuery/Algorithms.lean @@ -504,7 +504,7 @@ lemma sum_prod_majority_le {k t : ℕ} {ε : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε have hne : y j ≠ b j := by simpa [hS] using (Finset.mem_filter.mp hj).2 have hval : y j = !(b j) := by - cases hb : b j <;> cases hyj : y j <;> simp_all + exact Bool.eq_not_of_ne hne rw [hval] exact hpe j have h2 : (∏ j ∈ Sᶜ, p j (y j)) ≤ 1 := @@ -1509,19 +1509,19 @@ private lemma blockDiagonal_mulVec_embed rw [Matrix.blockDiagonal_apply] by_cases h : u' = u · subst h - by_cases h2 : u' = v <;> simp [h2] - · simp [h, Ne.symm h] + by_cases h2 : u' = v <;> simp only [h2, ↓reduceIte, mul_zero] + · simp only [ite_eq_right h, ite_eq_right (Ne.symm h), zero_mul] simp only [hterm] rw [show (∑ s : QBasis ι σ W, ∑ u : V, (if u = u' then (if u' = v then fam u' s' s * ψ s else 0) else 0)) = ∑ s : QBasis ι σ W, (if u' = v then fam u' s' s * ψ s else 0) from Finset.sum_congr rfl fun s _ => by rw [Finset.sum_ite_eq' Finset.univ u' (fun _ => (if u' = v then fam u' s' s * ψ s else 0))] - simp] + simp only [Finset.mem_univ, ↓reduceIte]] by_cases h : u' = v · subst h - simp [Matrix.mulVec, dotProduct] - · simp [h] + simp only [Matrix.mulVec, dotProduct, ↓reduceIte] + · simp only [ite_eq_right h, Finset.sum_const_zero] omit [DecidableEq W] [DecidableEq ι] [DecidableEq σ] in /-- **The action on the encoded subspace.** -/ @@ -4101,7 +4101,7 @@ theorem pairRoutine_run_prodState (R₁ : QRoutine ι σ W₁) rw [pairRoutine, QRoutine.comp_run, QRoutine.comp_run, QRoutine.comp_run, QRoutine.comp_run, QRoutine.comp_run, QRoutine.ofUnitary_run, QRoutine.ofUnitary_run] - noncomm_ring + simp only [Matrix.mul_assoc] rw [hrun, ← Matrix.mulVec_mulVec, ← Matrix.mulVec_mulVec, ← Matrix.mulVec_mulVec, ← Matrix.mulVec_mulVec, ← Matrix.mulVec_mulVec, pairSwap₁_mulVec_prodState] diff --git a/LeanPool/QuantumQuery/QueryBounds.lean b/LeanPool/QuantumQuery/QueryBounds.lean index 41face22ec..e773314bb4 100644 --- a/LeanPool/QuantumQuery/QueryBounds.lean +++ b/LeanPool/QuantumQuery/QueryBounds.lean @@ -1161,8 +1161,8 @@ private lemma sqrt_cross_sum_le {β β' ε : ℝ} (hβ0 : 0 ≤ β) (hβ'0 : 0 Real.sqrt (1 - β) * Real.sqrt β' + Real.sqrt β * Real.sqrt (1 - β') ≤ 2 * Real.sqrt (ε * (1 - ε)) := by have hε0 : 0 ≤ ε := le_trans hβ0 hβε - have hβ1 : β ≤ 1 := by linarith - have hβ'1 : β' ≤ 1 := by linarith + have hβ1 : β ≤ 1 := hβε.trans (hε2.trans (by norm_num)) + have hβ'1 : β' ≤ 1 := hβ'ε.trans (hε2.trans (by norm_num)) set s := Real.sqrt β with hs set s' := Real.sqrt β' with hs' set c := Real.sqrt (1 - β) with hc @@ -1174,8 +1174,8 @@ private lemma sqrt_cross_sum_le {β β' ε : ℝ} (hβ0 : 0 ≤ β) (hβ'0 : 0 have hc'0 : 0 ≤ c' := Real.sqrt_nonneg _ have hs2 : s ^ 2 = β := Real.sq_sqrt hβ0 have hs'2 : s' ^ 2 = β' := Real.sq_sqrt hβ'0 - have hc2 : c ^ 2 = 1 - β := Real.sq_sqrt (by linarith) - have hc'2 : c' ^ 2 = 1 - β' := Real.sq_sqrt (by linarith) + have hc2 : c ^ 2 = 1 - β := Real.sq_sqrt (sub_nonneg.mpr hβ1) + have hc'2 : c' ^ 2 = 1 - β' := Real.sq_sqrt (sub_nonneg.mpr hβ'1) have he2 : e ^ 2 = ε := Real.sq_sqrt hε0 have hse : s ≤ e := by rw [hs, he]; exact Real.sqrt_le_sqrt hβε have hs'e : s' ≤ e := by rw [hs', he]; exact Real.sqrt_le_sqrt hβ'ε @@ -1186,7 +1186,7 @@ private lemma sqrt_cross_sum_le {β β' ε : ℝ} (hβ0 : 0 ≤ β) (hβ'0 : 0 rw [show (c - c') ^ 2 = c ^ 2 - 2 * (c * c') + c' ^ 2 from by ring, hc2, hc'2] at hsq rw [hs2, hs'2] - linarith + linarith only [hsq] -- the squared left side, against the polynomial have hLsq : (c * s' + s * c') ^ 2 ≤ (s + s') ^ 2 * (1 - s * s') := by have h1 : (c * s' + s * c') ^ 2 @@ -1201,14 +1201,16 @@ private lemma sqrt_cross_sum_le {β β' ε : ℝ} (hβ0 : 0 ≤ β) (hβ'0 : 0 + 2 * (s * s') * (1 - (s ^ 2 + s' ^ 2) / 2) = (s + s') ^ 2 * (1 - s * s') := by rw [← hs2, ← hs'2]; ring - linarith [h1, h2, h3] + rw [h1, ← h3] + exact add_le_add_right h2 _ have hpoly := poly_bound hs0 hs'0 hse hs'e heh -- conclude by monotone square root have hL0 : 0 ≤ c * s' + s * c' := add_nonneg (mul_nonneg hc0 hs'0) (mul_nonneg hs0 hc'0) have hchain : (c * s' + s * c') ^ 2 ≤ (2 * Real.sqrt (ε * (1 - ε))) ^ 2 := by have hRsq : (2 * Real.sqrt (ε * (1 - ε))) ^ 2 = 4 * (ε * (1 - ε)) := by - rw [mul_pow, Real.sq_sqrt (by nlinarith : (0 : ℝ) ≤ ε * (1 - ε))] + rw [mul_pow, Real.sq_sqrt + (mul_nonneg hε0 (sub_nonneg.mpr (hε2.trans (by norm_num))))] norm_num rw [hRsq] calc (c * s' + s * c') ^ 2 ≤ (s + s') ^ 2 * (1 - s * s') := hLsq diff --git a/LeanPool/QuantumQuery/StateConversion.lean b/LeanPool/QuantumQuery/StateConversion.lean index 2235e96f5d..d32aa2cd82 100644 --- a/LeanPool/QuantumQuery/StateConversion.lean +++ b/LeanPool/QuantumQuery/StateConversion.lean @@ -787,7 +787,9 @@ theorem effective_chord_gap_sq {P L : Matrix H H ℂ} (hP : IsQProjector P) norm_num have hbound := chordNear_bound_sq U Δ w have hproj := (isQProjector_chordNearProj U Δ).qNormSq_mulVec_le w - nlinarith [sq_nonneg Δ, qNormSq_nonneg (N *ᵥ (P *ᵥ w)), qNormSq_nonneg w] + have htotal := h4.le.trans + (hbound.trans (mul_le_mul_of_nonneg_left hproj (sq_nonneg Δ))) + linarith only [htotal] end QuantumQueryComplexity @@ -4950,7 +4952,7 @@ theorem qNormSq_uniformConvError_le_sixteenth (P : DualPairOn read K f) {c : ℝ} (hP : P.IsCostLe c) (hc : 0 ≤ c) (x : X) : qNormSq (uniformConvError P (uniformAlpha c) (uniformT c) x) ≤ 1 / 16 := by - have hB0 : (0 : ℝ) < 1 + c := by linarith + have hB0 : (0 : ℝ) < 1 + c := by linarith only [hc] have hα := uniformAlpha_ne_zero hc have hαsq := uniformAlpha_sq hc have hT := uniformT_pos hc @@ -4961,12 +4963,12 @@ theorem qNormSq_uniformConvError_le_sixteenth (P : DualPairOn read K f) rw [hαsq, show (8 : ℝ) * (128 * (1 + c))⁻¹ * c = 8 * c / (128 * (1 + c)) from by rw [div_eq_mul_inv]; ring, div_le_div_iff₀ (by linarith) (by norm_num : (0 : ℝ) < 16)] - linarith + linarith only -- the near coefficient: `1 + c/(2α²) = 1 + 64c(1+c) ≤ 64(1+c)²` have hval : 1 + c / (2 * uniformAlpha c ^ 2) ≤ 64 * (1 + c) ^ 2 := by rw [hαsq, show c / (2 * (128 * (1 + c))⁻¹) = 64 * c * (1 + c) from by rw [div_eq_mul_inv, mul_inv, inv_inv]; ring] - nlinarith + nlinarith only [hc] have hsqrt : Real.sqrt (1 + c / (2 * uniformAlpha c ^ 2)) ≤ 8 * (1 + c) := by calc Real.sqrt (1 + c / (2 * uniformAlpha c ^ 2)) @@ -5000,19 +5002,19 @@ theorem qNormSq_uniformConvError_le_sixteenth (P : DualPairOn read K f) _ ≤ (uniformT c : ℝ) * uniformDelta c := mul_le_mul_of_nonneg_right hTge hΔ.le have hfar : 4 / ((uniformT c : ℝ) * uniformDelta c) ≤ 1 / 8 := by - rw [div_le_div_iff₀ (by linarith) (by norm_num : (0 : ℝ) < 8)] - linarith + rw [div_le_div_iff₀ (lt_of_lt_of_le (by norm_num : (0 : ℝ) < 32) hTΔ) + (by norm_num : (0 : ℝ) < 8)] + linarith only [hTΔ] -- square the `e₋` budget and combine through the exact half-sum have hn0 : 0 ≤ uniformDelta c * Real.sqrt (1 + c / (2 * uniformAlpha c ^ 2)) := mul_nonneg hΔ.le (Real.sqrt_nonneg _) - have hf0 : 0 ≤ 4 / ((uniformT c : ℝ) * uniformDelta c) := by - have : (0 : ℝ) < (uniformT c : ℝ) * uniformDelta c := by linarith - positivity + have hf0 : 0 ≤ 4 / ((uniformT c : ℝ) * uniformDelta c) := + div_nonneg (by norm_num) (le_trans (by norm_num) hTΔ) have hsq : (uniformDelta c * Real.sqrt (1 + c / (2 * uniformAlpha c ^ 2)) + 4 / ((uniformT c : ℝ) * uniformDelta c)) ^ 2 ≤ 1 / 16 := by - nlinarith [hnear, hfar, hn0, hf0] - linarith + nlinarith only [hnear, hfar, hn0, hf0] + linarith only [h, h1, hsq] /-- **The detector at the chosen clock stays within the acceptance budget**: `4(T − 1) ≤ 8192(1 + c)` — the @@ -5347,7 +5349,8 @@ theorem exists_algorithm_of_dualPairOn {c : ℝ} (P : DualPairOn read K f) set B : ℝ := 1 + 16 * (Fintype.card σ : ℝ) * c ^ 2 with hB have hB1 : (1 : ℝ) ≤ B := by rw [hB] - nlinarith [hσ, sq_nonneg c] + have hnonneg : 0 ≤ 16 * (Fintype.card σ : ℝ) * c ^ 2 := by positivity + linarith only [hnonneg] have hBs1 : (1 : ℝ) ≤ Real.sqrt B := by rw [show (1 : ℝ) = Real.sqrt 1 from (Real.sqrt_one).symm] exact Real.sqrt_le_sqrt hB1 @@ -5373,21 +5376,21 @@ theorem exists_algorithm_of_dualPairOn {c : ℝ} (P : DualPairOn read K f) = (((Fintype.card σ : ℝ) - 1) / (Fintype.card σ : ℝ)) * 16⁻¹ from by rw [mul_inv]; ring] have h2 : ((Fintype.card σ : ℝ) - 1) / (Fintype.card σ : ℝ) ≤ 1 := by - rw [div_le_one hσ]; linarith - nlinarith [h2] + rw [div_le_one hσ]; linarith only + linarith only [h2] have hden : (0 : ℝ) < 1 + ((Fintype.card σ : ℝ) - 1) * (16 * (Fintype.card σ : ℝ))⁻¹ := by have h0 : (0 : ℝ) ≤ ((Fintype.card σ : ℝ) - 1) * (16 * (Fintype.card σ : ℝ))⁻¹ := by have h1 : (1 : ℝ) ≤ (Fintype.card σ : ℝ) := by exact_mod_cast Fintype.card_pos_iff.mpr ‹Nonempty σ› - have : (0 : ℝ) ≤ (Fintype.card σ : ℝ) - 1 := by linarith + have : (0 : ℝ) ≤ (Fintype.card σ : ℝ) - 1 := sub_nonneg.mpr h1 positivity - linarith + linarith only [h0] rw [le_div_iff₀ hden] - nlinarith [hle] + linarith only [hle] have hsqB : Real.sqrt B * Real.sqrt B = B := - Real.mul_self_sqrt (by linarith) + Real.mul_self_sqrt (zero_le_one.trans hB1) have hneg : Δ / 4 * Real.sqrt (1 + 16 * (Fintype.card σ : ℝ) * c ^ 2) + 2 / ((T : ℝ) * Δ) + Δ ^ 2 / 8 * (1 + 16 * (Fintype.card σ : ℝ) * c ^ 2) ≤ 1 / 16 := by @@ -5395,12 +5398,12 @@ theorem exists_algorithm_of_dualPairOn {c : ℝ} (P : DualPairOn read K f) have e1 : Δ / 4 * Real.sqrt B = 1 / 64 := by rw [hΔdef] field_simp - linarith [hsqB] + linarith only [hsqB] have e2 : Δ ^ 2 / 8 * B = 1 / 2048 := by - rw [hΔdef, inv_pow, mul_pow, Real.sq_sqrt (by linarith : (0 : ℝ) ≤ B)] + rw [hΔdef, inv_pow, mul_pow, Real.sq_sqrt (zero_le_one.trans hB1)] rw [show ((16 : ℝ) ^ 2 * B)⁻¹ / 8 * B = B / B * (2048 : ℝ)⁻¹ from by rw [mul_inv]; ring] - rw [div_self (by linarith : B ≠ 0)] + rw [div_self (lt_of_lt_of_le one_pos hB1).ne'] norm_num have e3 : 2 / ((T : ℝ) * Δ) ≤ 1 / 64 := by have hT0 : (0 : ℝ) < (T : ℝ) := by exact_mod_cast hT @@ -5411,7 +5414,7 @@ theorem exists_algorithm_of_dualPairOn {c : ℝ} (P : DualPairOn read K f) calc 2 * (16 * Real.sqrt B) * 64 = 2048 * Real.sqrt B := by ring _ ≤ (T : ℝ) := hTge _ = 1 * (T : ℝ) := (one_mul _).symm - linarith [e1, e2, e3] + linarith only [e1, e2, e3] -- assemble have halg := scAlg_computes read f Q hT hΔ hcu hcv hpos hneg refine ⟨4 * (T - 1), mem_queryCounts halg, ?_⟩ @@ -5421,19 +5424,21 @@ theorem exists_algorithm_of_dualPairOn {c : ℝ} (P : DualPairOn read K f) norm_num have hBle : Real.sqrt B ≤ 1 + 4 * Real.sqrt (Fintype.card σ) * c := by have hsq : B ≤ (1 + 4 * Real.sqrt (Fintype.card σ) * c) ^ 2 := by - have hs : Real.sqrt (Fintype.card σ) * Real.sqrt (Fintype.card σ) - = (Fintype.card σ : ℝ) := Real.mul_self_sqrt hσ.le - have hs0 : (0 : ℝ) ≤ Real.sqrt (Fintype.card σ) := Real.sqrt_nonneg _ - rw [hB] - nlinarith [hs, hs0, hc.le] + have hs : (4 * Real.sqrt (Fintype.card σ) * c) ^ 2 + = 16 * (Fintype.card σ : ℝ) * c ^ 2 := by + rw [mul_pow, mul_pow, Real.sq_sqrt hσ.le] + norm_num + rw [hB, ← hs] + nlinarith only [mul_nonneg (Real.sqrt_nonneg (Fintype.card σ : ℝ)) hc.le] calc Real.sqrt B ≤ Real.sqrt ((1 + 4 * Real.sqrt (Fintype.card σ) * c) ^ 2) := Real.sqrt_le_sqrt hsq _ = 1 + 4 * Real.sqrt (Fintype.card σ) * c := by rw [Real.sqrt_sq (by positivity)] rw [hT1] - calc 4 * ((T : ℝ) - 1) ≤ 4 * (2048 * Real.sqrt B) := by linarith [hTle] + calc 4 * ((T : ℝ) - 1) ≤ 4 * (2048 * Real.sqrt B) := by linarith only [hTle] _ = 8192 * Real.sqrt B := by ring - _ ≤ 8192 * (1 + 4 * Real.sqrt (Fintype.card σ) * c) := by linarith [hBle] + _ ≤ 8192 * (1 + 4 * Real.sqrt (Fintype.card σ) * c) := + mul_le_mul_of_nonneg_left hBle (by norm_num) omit [DecidableEq K] [DecidableEq X] in /-- **The `qQueryOn` corollary**: `Q_{1/16}(f) ≤ 8192(1 + 4√|σ|·c)` for any