From a5f259bf1170d7a7e1f11811d3b322493f1403b8 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sun, 18 Oct 2026 13:23:36 +0000 Subject: [PATCH] Optimize QuantumParallelRepetition proof elaboration --- .../QuantumParallelRepetition/Part01.lean | 171 ++++++------- .../QuantumParallelRepetition/Part02.lean | 165 ++++++------- .../QuantumParallelRepetition/Part03.lean | 129 ++++------ .../QuantumParallelRepetition/Part04.lean | 93 ++++--- .../QuantumParallelRepetition/Part05.lean | 97 ++++---- .../QuantumParallelRepetition/Part06.lean | 70 +++--- .../QuantumParallelRepetition/Part07.lean | 226 +++++------------- .../QuantumParallelRepetition/Part08.lean | 74 +++--- .../QuantumParallelRepetition/Part09.lean | 185 ++++++-------- .../QuantumParallelRepetition/Part10.lean | 207 +++++++--------- 10 files changed, 578 insertions(+), 839 deletions(-) diff --git a/LeanPool/QuantumParallelRepetition/Part01.lean b/LeanPool/QuantumParallelRepetition/Part01.lean index f6e1a3f111..68769fb3eb 100644 --- a/LeanPool/QuantumParallelRepetition/Part01.lean +++ b/LeanPool/QuantumParallelRepetition/Part01.lean @@ -241,7 +241,7 @@ theorem winProbability_nonneg (S : Strategy G) : 0 ≤ S.winProbability := by refine Finset.sum_nonneg fun x _ => Finset.sum_nonneg fun y _ => ?_ apply mul_nonneg (G.weight_nonneg x y) exact Finset.sum_nonneg fun a _ => Finset.sum_nonneg fun b _ => by - split <;> simp [S.outcomeProbability_nonneg] + split <;> simp only [S.outcomeProbability_nonneg, Std.le_refl] theorem winProbability_le_one (S : Strategy G) : S.winProbability ≤ 1 := by classical @@ -462,7 +462,7 @@ theorem winningEffect_born intro a _ apply Finset.sum_congr rfl intro b _ - split <;> simp + split <;> simp only [Matrix.trace_zero, Complex.zero_re] theorem winProbability_eq_winningEffect_born (S : Strategy G) : @@ -757,7 +757,7 @@ private theorem convexMixtureStrategy_winProbability ∑ j : J, p j * (if G.predicate x y a b = true then (S j).outcomeProbability x y a b else 0) := by - split <;> simp + split <;> simp only [mul_zero, Finset.sum_const_zero] have h_swap (f : X → Y → A → B → J → ℝ) : (∑ x : X, ∑ y : Y, ∑ a : A, ∑ b : B, ∑ j : J, f x y a b j) = @@ -807,7 +807,7 @@ private theorem convexMixtureStrategy_winProbability intro a _ apply Finset.sum_congr rfl intro b _ - ring + ac_rfl end @@ -1065,7 +1065,7 @@ theorem exists_greedy_stopping [Fintype ι] [DecidableEq ι] (sub_nonneg.mpr hη_one) _ = (1 - η) ^ (insert i D).card := by rw [Finset.card_insert_of_notMem hi_not, pow_succ] - ring + ac_rfl have hnext_mem : insert i D ∈ candidates := by simp only [candidates, Finset.mem_filter, Finset.mem_powerset] exact ⟨Finset.subset_univ _, hnext_card, hnext_bound⟩ @@ -1186,7 +1186,7 @@ private theorem strategyEventLaw_winEvent rw [Finset.mul_sum] apply Finset.sum_congr rfl intro b _ - split <;> simp + split <;> simp only [mul_zero] /-- The repeated coordinate win construction used in the quantum parallel-repetition argument. -/ def repeatedCoordinateWin (G : Game X Y A B) (n : ℕ) @@ -1531,7 +1531,7 @@ theorem scalar_resolvent_purification_integrable_of_pos IntegrableOn (fun s : ℝ => (s + z) ^ (-2 : ℝ)) (Ioi 0) := by exact integrableOn_add_rpow_Ioi_of_lt (a := (-2 : ℝ)) (c := (0 : ℝ)) (m := z) - (by norm_num) (by linarith) + (by norm_num) (by linarith only [hz]) have hscaled : IntegrableOn (fun s : ℝ => z ^ 2 * (s + z) ^ (-2 : ℝ)) (Ioi 0) := @@ -1539,7 +1539,7 @@ theorem scalar_resolvent_purification_integrable_of_pos refine hscaled.congr_fun (fun s hs => ?_) measurableSet_Ioi have hspos : 0 < s + z := by have : 0 < s := hs - linarith + linarith only [hz, this] change z ^ 2 * (s + z) ^ (-2 : ℝ) = (z / (z + s)) ^ 2 rw [show (-2 : ℝ) = -(2 : ℝ) by norm_num, Real.rpow_neg hspos.le, Real.rpow_two] @@ -1568,7 +1568,7 @@ theorem scalar_resolvent_purification_integral intro x hx have hden : z + x ≠ 0 := by have hx_nonneg : 0 ≤ x := hx - exact ne_of_gt (by linarith) + exact ne_of_gt (by linarith only [hzpos, hx_nonneg]) have hd := ((hasDerivAt_const x (-(z ^ 2))).div ((hasDerivAt_const x z).add (hasDerivAt_id x)) hden) have hfun : @@ -1895,7 +1895,7 @@ theorem marginalX_mul_conditionalYGivenX have hle := G.questionWeight_le_marginalX x y have hnonneg := G.weight_nonneg x y rw [hx] at hle - linarith + linarith only [hnonneg, hle] simp only [hx, hzero, div_zero, mul_zero] · field_simp @@ -1909,7 +1909,7 @@ theorem marginalY_mul_conditionalXGivenY have hle := G.questionWeight_le_marginalY x y have hnonneg := G.weight_nonneg x y rw [hy] at hle - linarith + linarith only [hnonneg, hle] simp only [hy, hzero, div_zero, mul_zero] · field_simp @@ -2124,7 +2124,7 @@ theorem conditionedAliceEffect_complement_positive ← Finset.sum_sub_distrib] apply Finset.sum_congr rfl intro answers _ - split_ifs <;> simp + split_ifs <;> simp only [sub_self, sub_zero] rw [hsplit] apply Matrix.posSemidef_sum Finset.univ intro answers _ @@ -2152,7 +2152,7 @@ theorem conditionedBobEffect_complement_positive ← Finset.sum_sub_distrib] apply Finset.sum_congr rfl intro answers _ - split_ifs <;> simp + split_ifs <;> simp only [sub_self, sub_zero] rw [hsplit] apply Matrix.posSemidef_sum Finset.univ intro answers _ @@ -2332,7 +2332,8 @@ private theorem spectralSupportProjection_mul _ = spectralSupportFunctional F hF (fun x => x) := spectralSupportFunctional_congr F hF (by intro i - by_cases hi : hF.isHermitian.eigenvalues i = 0 <;> simp [hi]) + by_cases hi : hF.isHermitian.eigenvalues i = 0 <;> simp only [hi, ↓reduceIte, mul_zero, + one_mul]) _ = F := spectralSupportFunctional_id F hF private theorem spectralSupportInverse_penrose @@ -3110,7 +3111,7 @@ theorem fullHistoryWeight_mul_hidden G.marginalY (h.bobRemaining i)) * (∏ i : {i : Fin n // i ∈ fullHistoryRemaining n D L}, G.conditionalXGivenY - (h.bobRemaining i) (hx i))) := by ring + (h.bobRemaining i) (hx i))) := by ac_rfl _ = (∏ i ∈ D, q i) * (∏ i ∈ L, q i) * (∏ i ∈ fullHistoryRemaining n D L, q i) := by @@ -3496,7 +3497,7 @@ theorem fullHistoryFilters_born_expansion intro hx _ apply Finset.sum_congr rfl intro hy _ - ring + ac_rfl theorem fullSubsetHistory_mass_eq_postselection (G : Game X Y A B) (n : ℕ) @@ -3587,7 +3588,7 @@ theorem fullSubsetHistory_mass_eq_postselection intro β _ rw [fullHistoryWinIndicator_eq_question G D L h hx hy α β] rw [← fullHistoryWeight_mul_hidden G D L hL h hx hy] - ring + ac_rfl _ = ∑ xs : Fin n → X, ∑ ys : Fin n → Y, ∑ α : {i : Fin n // i ∈ D} → A, ∑ β : {i : Fin n // i ∈ D} → B, @@ -3732,44 +3733,22 @@ theorem spectralPurificationFilter_square_contraction have hDstar : star D = D := by simpa only [Matrix.star_eq_conjTranspose] using hDhermitian.eq have hdiag : (D - D * D).PosSemidef := by - rw [show D * D = Matrix.diagonal (fun i => - (((eigenvalue i / (eigenvalue i + s)) ^ 2 : ℝ) : ℂ)) by - dsimp [D] - rw [Matrix.diagonal_mul_diagonal] - congr 1 - funext i - simp only [Complex.ofReal_div, Complex.ofReal_add, pow_two, Complex.ofReal_mul]] - have hsub : D - Matrix.diagonal (fun i => - (((eigenvalue i / (eigenvalue i + s)) ^ 2 : ℝ) : ℂ)) = - Matrix.diagonal (fun i => - ((eigenvalue i / (eigenvalue i + s) - - (eigenvalue i / (eigenvalue i + s)) ^ 2 : ℝ) : ℂ)) := by - ext i j - by_cases hij : i = j - · subst j - simp only [Complex.ofReal_div, Complex.ofReal_add, Complex.ofReal_pow, Matrix.sub_apply, - Matrix.diagonal_apply_eq, Complex.ofReal_sub, D] - · simp only [Complex.ofReal_div, Complex.ofReal_add, Complex.ofReal_pow, Matrix.sub_apply, - ne_eq, hij, not_false_eq_true, Matrix.diagonal_apply_ne, sub_self, Complex.ofReal_sub, - D] - rw [hsub] + dsimp only [D] + rw [Matrix.diagonal_mul_diagonal, Matrix.diagonal_sub] apply Matrix.PosSemidef.diagonal intro i - change 0 ≤ ((eigenvalue i / (eigenvalue i + s) - - (eigenvalue i / (eigenvalue i + s)) ^ 2 : ℝ) : ℂ) - apply Complex.nonneg_iff.mpr - constructor - · have hnonneg : 0 ≤ eigenvalue i / (eigenvalue i + s) := - div_nonneg (hF.eigenvalues_nonneg i) - (le_of_lt (add_pos_of_nonneg_of_pos - (hF.eigenvalues_nonneg i) hs)) - have hle : eigenvalue i / (eigenvalue i + s) ≤ 1 := - (div_le_one (add_pos_of_nonneg_of_pos - (hF.eigenvalues_nonneg i) hs)).mpr (by linarith) - change 0 ≤ eigenvalue i / (eigenvalue i + s) - - (eigenvalue i / (eigenvalue i + s)) ^ 2 - nlinarith - · simp only [Complex.ofReal_im] + change 0 ≤ ((eigenvalue i / (eigenvalue i + s) : ℝ) : ℂ) - + ((eigenvalue i / (eigenvalue i + s) : ℝ) : ℂ) * + ((eigenvalue i / (eigenvalue i + s) : ℝ) : ℂ) + rw [← Complex.ofReal_mul, ← Complex.ofReal_sub] + have hnonneg : 0 ≤ eigenvalue i / (eigenvalue i + s) := + div_nonneg (hF.eigenvalues_nonneg i) + (le_of_lt (add_pos_of_nonneg_of_pos (hF.eigenvalues_nonneg i) hs)) + have hle : eigenvalue i / (eigenvalue i + s) ≤ 1 := + (div_le_one (add_pos_of_nonneg_of_pos (hF.eigenvalues_nonneg i) hs)).mpr + (le_add_of_nonneg_right hs.le) + exact Complex.nonneg_iff.mpr + ⟨sub_nonneg.mpr (mul_le_of_le_one_right hnonneg hle), rfl⟩ change (e D - star (e D) * e D).PosSemidef rw [← map_star, hDstar, ← map_mul, ← map_sub] change ((U : Matrix d d ℂ) * (D - D * D) * @@ -3837,12 +3816,8 @@ theorem bochner_integral_posSemidef filter_upwards [hpos] with t ht simpa only [Matrix.star_eq_conjTranspose] using ht.isHermitian.eq have hhermitian : (∫ t, f t ∂μ).IsHermitian := by - apply Matrix.IsHermitian.ext - intro i j - have hstar : star (∫ t, f t ∂μ) = ∫ t, f t ∂μ := - hadjoint.trans (integral_congr_ae hadjoint_ae) - have hentry := congr_fun (congr_fun hstar i) j - simpa only [RCLike.star_def, Matrix.star_apply] using hentry + change star (∫ t, f t ∂μ) = ∫ t, f t ∂μ + exact hadjoint.trans (integral_congr_ae hadjoint_ae) apply Matrix.PosSemidef.of_dotProduct_mulVec_nonneg hhermitian intro x have hcomm : @@ -4032,7 +4007,7 @@ theorem weighted_shifted_inverse_second_order (fun i => Matrix.nonsing_inv_mul _ (hdetF i)) (Matrix.mul_nonsing_inv _ hdetM) (Matrix.nonsing_inv_mul _ hdetM) - simpa [W, RF, RM, smul_mul_assoc] using hidentity + simpa only [W, RF, RM, smul_mul_assoc, one_mul] using hidentity theorem weighted_spectralPurificationFilter_variance_le_inverse_jensen {ι d : Type*} [Fintype ι] [Fintype d] [DecidableEq d] @@ -4239,8 +4214,6 @@ theorem scalar_entropy_resolvent_integrable (Ioi 0) := hproduct.const_mul (z - 1) refine hscaled.congr_fun (fun s hs => ?_) measurableSet_Ioi have hspos : 0 < s := hs - have hzone : 1 + s ≠ 0 := ne_of_gt (by linarith) - have hzden : z + s ≠ 0 := ne_of_gt (by linarith) field_simp ring @@ -4547,8 +4520,8 @@ theorem scalar_entropy_resolvent_integral (z / (1 + x) - z / (z + x)) x := by intro x hx have hxnonneg : 0 ≤ x := hx - have hnum : 1 + x ≠ 0 := ne_of_gt (by linarith) - have hden : z + x ≠ 0 := ne_of_gt (by linarith) + have hnum : 1 + x ≠ 0 := ne_of_gt (by linarith only [hxnonneg]) + have hden : z + x ≠ 0 := ne_of_gt (by linarith only [hzpos, hxnonneg]) have hratio : (1 + x) / (z + x) ≠ 0 := div_ne_zero hnum hden have hdnum := @@ -4583,7 +4556,7 @@ theorem scalar_entropy_resolvent_integral simpa only [add_zero] using hone.add hzero apply h'.congr' filter_upwards [eventually_gt_atTop (-z)] with t ht - have hden : z + t ≠ 0 := ne_of_gt (by linarith) + have hden : z + t ≠ 0 := ne_of_gt (by linarith only [ht]) field_simp ring have hlog_limit : @@ -5245,7 +5218,7 @@ private theorem leftSpectralBornWeight_moment apply Finset.sum_congr rfl intro i _ unfold leftSpectralBornWeight - ring + ac_rfl _ = bornTracePairing ρ.matrix F G := h.symm private theorem leftSpectralBornWeight_entropy @@ -5283,7 +5256,7 @@ private theorem leftSpectralBornWeight_entropy apply Finset.sum_congr rfl intro i _ unfold leftSpectralBornWeight - ring + ac_rfl theorem bornTracePairing_one_one {dA dB : Type*} @@ -5314,7 +5287,7 @@ theorem bornTracePairing_one_le_one bornTracePairing ρ.matrix (1 : Matrix dA dA ℂ) G := (bornTracePairing ρ.matrix (1 : Matrix dA dA ℂ)).map_sub 1 G rw [hdiff, bornTracePairing_one_one] at hpositive - linarith + linarith only [hpositive] theorem positiveContraction_eigenvalue_le_one {d : Type*} [Fintype d] [DecidableEq d] @@ -5491,7 +5464,8 @@ theorem rawEmbezzlementState_norm_sq (n : ℕ) : ‖(↑((Real.sqrt ((i.val : ℝ) + 1))⁻¹) : ℂ)‖ ^ 2 else 0 := by - split_ifs <;> simp + split_ifs <;> simp only [Complex.ofReal_inv, norm_inv, Complex.norm_real, Real.norm_eq_abs, + inv_pow, sq_abs, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow] rw [EuclideanSpace.norm_sq_eq, Fintype.sum_prod_type] unfold harmonicNumber apply Finset.sum_congr rfl @@ -5749,7 +5723,8 @@ theorem finiteTensorVector_norm ‖finiteTensorVector v‖ = 1 := by have hsquare := finiteTensorVector_norm_sq v simp_rw [hv, one_pow, Finset.prod_const_one] at hsquare - nlinarith [norm_nonneg (finiteTensorVector v)] + exact (sq_eq_sq₀ (norm_nonneg _) zero_le_one).mp (by + simpa only [one_pow] using hsquare) theorem spectralAtomOverlap_sum_right {d : Type*} [Fintype d] [DecidableEq d] @@ -5837,7 +5812,7 @@ theorem spectralAtomOverlap_schmidtMass_le_one rw [Finset.mul_sum] apply Finset.sum_congr rfl intro j _ - ring + ac_rfl _ = ∑ i : d, hF.isHermitian.eigenvalues i := by simp_rw [spectralAtomOverlap_sum_right, mul_one] @@ -5860,7 +5835,7 @@ theorem spectralAtomOverlap_schmidtMass_le_one rw [Finset.mul_sum] apply Finset.sum_congr rfl intro i _ - ring + ac_rfl _ = ∑ j : d, hG.isHermitian.eigenvalues j := by simp_rw [spectralAtomOverlap_sum_left, mul_one] @@ -5877,7 +5852,7 @@ theorem spectralAtomOverlap_schmidtMass_le_one apply Finset.sum_congr rfl intro j _ dsimp [w, f, g] - ring + ac_rfl _ ≤ Real.sqrt (∑ q : d × d, w q * f q ^ 2) * Real.sqrt (∑ q : d × d, w q * g q ^ 2) := by apply weighted_real_cauchy @@ -5987,10 +5962,11 @@ theorem unitVector_distance_of_real_overlap exact hoverlap have hsq : ‖z - w‖ ^ 2 ≤ 2 * ε := by rw [@norm_sub_sq ℂ, hz, hw] - linarith [hoverlap'] + linarith only [hoverlap'] have hsqrt : (Real.sqrt (2 * ε)) ^ 2 = 2 * ε := Real.sq_sqrt (by positivity) - nlinarith [norm_nonneg (z - w), Real.sqrt_nonneg (2 * ε)] + exact (sq_le_sq₀ (norm_nonneg _) (Real.sqrt_nonneg _)).mp + (hsq.trans_eq hsqrt.symm) /-- The shared threshold resource raw construction used in the quantum parallel-repetition argument. @@ -6361,7 +6337,7 @@ theorem doublyStochasticSchmidtMass_le_one rw [Finset.mul_sum] apply Finset.sum_congr rfl intro i _ - ring + ac_rfl _ = ∑ j : κ, μ j ^ 2 := by simp_rw [hcol, mul_one] _ = 1 := hμunit calc @@ -6373,7 +6349,7 @@ theorem doublyStochasticSchmidtMass_le_one apply Finset.sum_congr rfl intro j _ dsimp [W, f, g] - ring + ac_rfl _ ≤ Real.sqrt (∑ q : ι × κ, W q * f q ^ 2) * Real.sqrt (∑ q : ι × κ, W q * g q ^ 2) := by apply weighted_real_cauchy @@ -6454,8 +6430,8 @@ theorem complexInner_norm_sq_le (z w : EuclideanSpace ℂ ι) : ‖inner ℂ z w‖ ^ 2 ≤ ‖z‖ ^ 2 * ‖w‖ ^ 2 := by have hcauchy := @norm_inner_le_norm ℂ _ _ _ _ z w - nlinarith [norm_nonneg (inner ℂ z w), norm_nonneg z, - norm_nonneg w, mul_nonneg (norm_nonneg z) (norm_nonneg w)] + simpa only [mul_pow] using + (sq_le_sq₀ (norm_nonneg _) (mul_nonneg (norm_nonneg z) (norm_nonneg w))).mpr hcauchy private theorem twoSidedSchmidtSpectralEnergy_le {ι κ ν : Type*} [Fintype ι] [Fintype κ] [Fintype ν] @@ -6514,7 +6490,7 @@ private theorem twoSidedSchmidtSpectralEnergy_le σ μ hσ hμ L, weightedComplexOverlapVector_norm_sq σ μ hσ hμ R] - _ ≤ a := by nlinarith + _ ≤ a := mul_le_of_le_one_right ha hb have hre : (inner ℂ ψ φ).re ^ 2 ≤ a := by calc (inner ℂ ψ φ).re ^ 2 = @@ -6536,7 +6512,7 @@ private theorem twoSidedSchmidtSpectralEnergy_le hσunit hμunit hLrow hLcol, hdistance] change 2 - 2 * a ≤ 2 * (2 - 2 * (inner ℂ ψ φ).re) - linarith [sq_nonneg ((inner ℂ ψ φ).re - 1)] + linarith only [hre, sq_nonneg ((inner ℂ ψ φ).re - 1)] /-- The target object for tensor embezzlement. -/ def tensorEmbezzlementTarget @@ -6605,7 +6581,8 @@ theorem tensorEmbezzlementTarget_norm ← EuclideanSpace.norm_sq_eq, ← EuclideanSpace.norm_sq_eq, ξ.property, embezzlementState_norm n hn] norm_num - nlinarith [norm_nonneg (tensorEmbezzlementTarget (n := n) ξ)] + exact (sq_eq_sq₀ (norm_nonneg _) zero_le_one).mp (by + simpa only [one_pow] using hsquare) /-- The operator action for local unitary. -/ def localUnitaryAction {n : ℕ} @@ -6632,14 +6609,15 @@ theorem localUnitaryAction_norm {n : ℕ} (V : Matrix (Fin n) (Fin n) ℂ) have hM : M ∈ Matrix.unitaryGroup (Fin n × Fin n) ℂ := localUnitaryAction_matrix_mem_unitary U V - have hclm : Matrix.toEuclideanCLM - (n := Fin n × Fin n) (𝕜 := ℂ) M ∈ - unitary - (EuclideanSpace ℂ (Fin n × Fin n) →L[ℂ] - EuclideanSpace ℂ (Fin n × Fin n)) := - Unitary.map_mem - (Matrix.toEuclideanCLM (n := Fin n × Fin n) (𝕜 := ℂ)) hM - exact ContinuousLinearMap.norm_map_of_mem_unitary hclm ψ + have gram : M.conjTranspose * M = 1 := by + simpa only [Matrix.star_eq_conjTranspose] using (Matrix.mem_unitaryGroup_iff'.mp hM) + apply (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp + change ‖toLp 2 (M.mulVec (ofLp ψ))‖ ^ 2 = ‖ψ‖ ^ 2 + rw [rectangularMatrix_norm_sq, gram] + change (inner ℂ ψ (Matrix.toEuclideanCLM + (n := Fin n × Fin n) (𝕜 := ℂ) (1 : Matrix _ _ ℂ) ψ)).re = ‖ψ‖ ^ 2 + simp only [map_one, one_apply_eq_self, inner_self_eq_norm_sq_to_K, + Complex.coe_algebraMap, ← Complex.ofReal_pow, Complex.ofReal_re] theorem unitary_row_norm_sq_sum {d : Type*} [Fintype d] [DecidableEq d] @@ -6694,7 +6672,8 @@ theorem diagonalSchmidtState_norm_sq have hterm (j : d) : ‖if i = j then (σ i : ℂ) else 0‖ ^ 2 = if i = j then σ i ^ 2 else 0 := by - split_ifs <;> simp [Complex.norm_real, Real.norm_eq_abs, sq_abs] + split_ifs <;> simp only [Complex.norm_real, Real.norm_eq_abs, sq_abs, norm_zero, ne_eq, + OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow] simp_rw [hterm] simp only [Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte] @@ -6769,7 +6748,7 @@ private theorem weightedComplexOverlapVector_inner _ = ((Real.sqrt (σ i * μ j) : ℂ) * (Real.sqrt (σ i * μ j) : ℂ)) * - L i j * R i j := by ring + L i j * R i j := by ac_rfl _ = (σ i : ℂ) * (μ j : ℂ) * L i j * R i j := by rw [hsqrt] @@ -6903,11 +6882,13 @@ theorem schmidtVector_spectralEnergy_le have hψ : ‖schmidtVector σ U V‖ = 1 := by have h := schmidtVector_norm_sq σ U V rw [hσunit] at h - nlinarith [norm_nonneg (schmidtVector σ U V)] + exact (sq_eq_sq₀ (norm_nonneg _) zero_le_one).mp (by + simpa only [one_pow] using h) have hφ : ‖schmidtVector μ X Y‖ = 1 := by have h := schmidtVector_norm_sq μ X Y rw [hμunit] at h - nlinarith [norm_nonneg (schmidtVector μ X Y)] + exact (sq_eq_sq₀ (norm_nonneg _) zero_le_one).mp (by + simpa only [one_pow] using h) let L : Fin d → Fin d → ℂ := fun i j => star (unitaryBasisOverlap U X i j) let R : Fin d → Fin d → ℂ := @@ -7007,8 +6988,6 @@ theorem linearMap_exists_singularBases intro i j have hi : (σ (i : Fin d) : ℂ) ≠ 0 := by exact_mod_cast i.property - have hj : (σ (j : Fin d) : ℂ) ≠ 0 := by - exact_mod_cast j.property change inner ℂ (((σ (i : Fin d) : ℂ)⁻¹) • T (v i)) (((σ (j : Fin d) : ℂ)⁻¹) • T (v j)) = _ diff --git a/LeanPool/QuantumParallelRepetition/Part02.lean b/LeanPool/QuantumParallelRepetition/Part02.lean index 7d8beafab1..30081de174 100644 --- a/LeanPool/QuantumParallelRepetition/Part02.lean +++ b/LeanPool/QuantumParallelRepetition/Part02.lean @@ -55,7 +55,7 @@ theorem harmonicNumber_log_upper (n : ℕ) : theorem harmonicNumber_pos {n : ℕ} (hn : 0 < n) : 0 < harmonicNumber n := by have hnreal : 0 < (n : ℝ) := by exact_mod_cast hn - exact (Real.log_pos (by linarith : (1 : ℝ) < (n : ℝ) + 1)).trans_le + exact (Real.log_pos (by linarith only [hnreal] : (1 : ℝ) < (n : ℝ) + 1)).trans_le (harmonicNumber_log_lower n) theorem harmonicNumber_mul_le_add @@ -65,7 +65,7 @@ theorem harmonicNumber_mul_le_add have hdreal : 0 < (d : ℝ) := by exact_mod_cast hd have hnreal : 0 < (n : ℝ) := by exact_mod_cast hn have hlogn : Real.log (n : ℝ) ≤ harmonicNumber n := by - exact (Real.log_le_log hnreal (by linarith : + exact (Real.log_le_log hnreal (by linarith only [] : (n : ℝ) ≤ (n : ℝ) + 1)).trans (harmonicNumber_log_lower n) calc @@ -75,7 +75,7 @@ theorem harmonicNumber_mul_le_add _ = 1 + (Real.log (d : ℝ) + Real.log (n : ℝ)) := by rw [Nat.cast_mul, Real.log_mul hdreal.ne' hnreal.ne'] _ ≤ harmonicNumber n + (1 + Real.log (d : ℝ)) := by - linarith + linarith only [hlogn] theorem exists_proofHarmonicNumber_gt (bound : ℝ) : ∃ n : ℕ, bound < harmonicNumber n := by @@ -83,7 +83,7 @@ theorem exists_proofHarmonicNumber_gt (bound : ℝ) : have hpositive : 0 < (n : ℝ) + 1 := by positivity have hlog : bound < Real.log ((n : ℝ) + 1) := by apply (Real.lt_log_iff_exp_lt hpositive).mpr - exact lt_trans hn (by linarith) + exact lt_trans hn (by linarith only []) exact ⟨n, hlog.trans_le (harmonicNumber_log_lower n)⟩ theorem exists_proofHarmonicNumber_ratio_ge @@ -174,7 +174,8 @@ theorem ePRState_norm (m : ℕ) (hm : 0 < m) : simp_rw [hterm] simp only [sum_ite_eq, mem_univ, ↓reduceIte, sum_const, card_univ, Fintype.card_fin, nsmul_eq_mul, ne_eq, hmreal.ne', not_false_eq_true, mul_inv_cancel₀] - nlinarith [norm_nonneg (ePRState m)] + exact (sq_eq_sq₀ (norm_nonneg _) zero_le_one).mp (by + simpa only [one_pow] using hsquare) theorem permutationMatrix_mem_unitary {ι : Type*} [Fintype ι] [DecidableEq ι] @@ -281,8 +282,7 @@ theorem harmonicSchmidtFiber_count_sq_le mul_nonneg hx (Real.sqrt_nonneg _) have hs : (x * Real.sqrt ((j.val : ℝ) + 1)) ^ 2 ≤ a ^ 2 := by - linarith [mul_nonneg (sub_nonneg.mpr hscaled) - (add_nonneg ha hnonneg)] + linarith only [mul_nonneg (sub_nonneg.mpr hscaled) (add_nonneg ha hnonneg)] rw [mul_pow, Real.sq_sqrt hjpositive.le] at hs linarith have hcardreal : (S.card : ℝ) ≤ (j.val : ℝ) + 1 := by @@ -444,12 +444,11 @@ private theorem descendingHarmonicSchmidtAmplitude_le_harmonic have hsquare : (x * Real.sqrt ((k.val : ℝ) + 1)) ^ 2 ≤ 1 := by rw [mul_pow, Real.sq_sqrt hrank.le] - linarith + linarith only [hrankbound] have hnonneg : 0 ≤ x * Real.sqrt ((k.val : ℝ) + 1) := mul_nonneg hx hsqrt.le - nlinarith [sq_nonneg - (x * Real.sqrt ((k.val : ℝ) + 1) + 1)] + nlinarith only [hsquare, hnonneg] private def diagonalSchmidtUnitVector {d : ℕ} (σ : Fin d → ℝ) @@ -657,10 +656,9 @@ private theorem universalCatalystOverlap_eq_sum intro k _ rw [harmonicSchmidtPermutationAction_diagonal, diagonalSchmidtTensorTarget_diagonal] - simp only [ofReal_inv, real_smul, mul_comm, RCLike.inner_apply, map_mul, map_inv₀, - conj_ofReal, mul_left_comm, mul_assoc, mul_re, inv_re, ofReal_re, normSq_ofReal, - div_self_mul_self', inv_im, ofReal_im, neg_zero, zero_div, mul_zero, sub_zero, mul_im, - zero_mul, add_zero, universalCatalystOverlapTerm] + simp only [real_smul, RCLike.inner_apply, conj_ofReal, + ← ofReal_mul, ofReal_re, universalCatalystOverlapTerm] + ac_rfl private theorem universalCatalystOverlapTerm_lower {d n : ℕ} (σ : Fin d → ℝ) @@ -700,7 +698,7 @@ private theorem universalCatalystOverlapTerm_lower _ = universalCatalystOverlapTerm (n := n) σ k := by dsimp [c, a, h, universalCatalystOverlapTerm] - ring + ac_rfl private theorem universalDiagonalCatalystOverlap_lower {d n : ℕ} (hd : 0 < d) (hn : 0 < n) @@ -908,7 +906,7 @@ private theorem harmonicTargetLift_diagonal_action_apply rw [Finset.mul_sum] apply Finset.sum_congr rfl intro k _ - ring + ac_rfl private theorem harmonicTargetLift_diagonal_action {d n : ℕ} @@ -1016,11 +1014,9 @@ private theorem universalDiagonalCatalystOverlap_of_harmonic_ratio rawEmbezzlementState_norm_sq, rawEmbezzlementState_norm_sq] have hgoalnonneg : 0 ≤ 1 - δ := sub_nonneg.mpr hδone - have hgoalsquare : (1 - δ) ^ 2 ≤ 1 - δ := by - linarith [mul_nonneg hδ hgoalnonneg] have hqbound : 1 - δ ≤ q := by rw [← hqsquare] at hratio - nlinarith [sq_nonneg (q + (1 - δ))] + nlinarith only [hratio, hδ, hq] exact hqbound.trans (universalDiagonalCatalystOverlap_lower hd hn σ hσ hunit) @@ -1092,11 +1088,11 @@ theorem exists_proofUniversalHarmonicCatalyst (n := n) ξ σ hunit U V hξ have hdeltaeps : 2 * δ ≤ ε ^ 2 := by have hmin : δ ≤ ε ^ 2 / 2 := min_le_left _ _ - linarith + linarith only [hmin] have hsqrt : Real.sqrt (2 * δ) ≤ ε := by have hsq : (Real.sqrt (2 * δ)) ^ 2 = 2 * δ := Real.sq_sqrt (by positivity) - nlinarith [Real.sqrt_nonneg (2 * δ)] + nlinarith only [hdeltaeps, hsq, hε, Real.sqrt_nonneg (2 * δ)] calc ‖localUnitaryAction (LU * P) (LV * P) (embezzlementState (d * n)) - @@ -1263,7 +1259,7 @@ theorem spectralPartitionPOVM_weighted_trace_deficit_eq_mismatch rw [Finset.mul_sum] apply Finset.sum_congr rfl intro j _ - split_ifs <;> simp + split_ifs <;> simp only [mul_one, mul_zero] _ = ∑ j : d, ∑ k : κ, if binG j = k then τ k ^ 2 else 0 := Finset.sum_comm @@ -1356,7 +1352,7 @@ theorem spectralPartitionPOVM_weighted_trace_deficit_eq_mismatch rw [← Finset.sum_sub_distrib] apply Finset.sum_congr rfl intro j _ - split_ifs <;> simp [w] + split_ifs <;> simp only [sub_self, w, sub_zero] end @@ -1423,12 +1419,12 @@ theorem finiteUniformGrid_interval_card_le (Finset.mem_filter.mp last_mem).2.2 have spread : ((last.val : ℝ) - (first.val : ℝ)) * step ≤ hi - lo := by - linarith + linarith only [first_lower, last_upper] have scaled : (last.val : ℝ) - (first.val : ℝ) ≤ (hi - lo) / step := (le_div_iff₀ positive).2 spread - linarith + linarith only [real_cardinal, scaled] · have empty : selected = ∅ := Finset.not_nonempty_iff_eq_empty.mp present rw [empty, Finset.card_empty, Nat.cast_zero] @@ -1573,7 +1569,7 @@ theorem targetSpectralAtomOverlap_eq_basis_norm_sq apply Finset.sum_congr rfl intro b _ simp only [starRingEnd_apply, star_star] - ring + ac_rfl unfold spectralAtomOverlap rw [cross] have coeff : @@ -1972,7 +1968,9 @@ theorem dSVCanonicalFailurePrefix_norm_sq else 0 := by by_cases same : i = j · subst j - by_cases before : i.val < r.val <;> simp [before] + by_cases before : i.val < r.val <;> simp only [before, and_self, ↓reduceIte, norm_one, + one_pow, and_false, norm_zero, ne_eq, + OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow] · simp only [same, false_and, ↓reduceIte, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow] simp_rw [atom] @@ -2124,7 +2122,7 @@ theorem dSVMixedProjectorSuccessLoss_le_square 0 ≤ (Matrix.trace R).re - (Matrix.trace (P * R)).re := by simpa only [sub_nonneg, Matrix.sub_mul, one_mul, trace_sub, sub_re] using remainder rw [square] - linarith + linarith only [rest] theorem dSVWeightedMixedProjectorSuccessLoss_le_square {κ d : Type*} [Fintype κ] [Fintype d] @@ -2277,7 +2275,7 @@ theorem dSVRationalSoftPass_mem_unit constructor · exact div_nonneg nonnegative denominator.le · apply (div_le_iff₀ denominator).mpr - linarith + linarith only [positive] theorem dSVRationalSoftPass_sub {t a b : ℝ} (positive : 0 < t) @@ -2286,8 +2284,6 @@ theorem dSVRationalSoftPass_sub dSVRationalSoftPass t b = t * (a - b) / ((a + t) * (b + t)) := by unfold dSVRationalSoftPass - have da : a + t ≠ 0 := by linarith - have db : b + t ≠ 0 := by linarith field_simp ring @@ -2297,15 +2293,15 @@ theorem dSVRationalSoftPass_lipschitz |dSVRationalSoftPass t a - dSVRationalSoftPass t b| ≤ |a - b| / t := by have denominator : 0 < (a + t) * (b + t) := - mul_pos (by linarith) (by linarith) + mul_pos (by linarith only [positive, ha]) (by linarith only [positive, hb]) rw [dSVRationalSoftPass_sub positive ha hb, abs_div, abs_mul, abs_of_pos positive, abs_of_pos denominator] apply (div_le_iff₀ denominator).mpr rw [div_mul_eq_mul_div] apply (le_div_iff₀ positive).mpr have wide : t ^ 2 ≤ (a + t) * (b + t) := by - nlinarith [mul_nonneg ha hb] - linarith [mul_le_mul_of_nonneg_left wide (abs_nonneg (a - b))] + nlinarith only [mul_nonneg ha hb, positive, ha, hb] + linarith only [mul_le_mul_of_nonneg_left wide (abs_nonneg (a - b))] end @@ -2327,7 +2323,7 @@ theorem dSVAdaptiveSoft_sqrt_sub_sq_le_abs linarith [mul_nonneg sa (sub_nonneg.mpr roots)] · rw [abs_of_nonneg (sub_nonneg.mpr ordered)] have roots := Real.sqrt_le_sqrt ordered - linarith [mul_nonneg sb (sub_nonneg.mpr roots)] + linarith only [square_a, square_b, mul_nonneg sb (sub_nonneg.mpr roots)] end @@ -2443,7 +2439,7 @@ theorem dSVHeterogeneousRealStopping_escape_budget dSVHeterogeneousRealPrefix continuation k * (1 - continuation k) := by apply mul_le_mul_of_nonneg_left - · linarith [escape_bound k] + · linarith only [escape_bound k] · exact dSVHeterogeneousRealPrefix_nonneg continuation continuation_nonnegative k calc @@ -2459,7 +2455,7 @@ theorem dSVHeterogeneousRealStopping_escape_budget _ ≤ 1 := by have := dSVHeterogeneousRealPrefix_nonneg continuation continuation_nonnegative N - linarith + linarith only [this] end @@ -2727,7 +2723,7 @@ private theorem dSVUniformDensitySchmidtSumMass_le_four intro j _ ring rw [split, left, right] - linarith + linarith only [cross] private theorem dSVUniformDensitySpectralAtomDiscrepancy_le {d : ℕ} (ξ ζ : BipartiteUnitVector d) : @@ -2765,7 +2761,7 @@ private theorem dSVUniformDensitySpectralAtomDiscrepancy_le (σ i - μ j) * (σ i + μ j) := by ring rw [factor, abs_mul, abs_of_nonneg sum_nonnegative] dsimp [weight, f, g, F, G, hF, hG, σ, μ] - ring + ac_rfl have exact_energy : (∑ ij : Fin d × Fin d, weight ij * f ij ^ 2) = targetCanonicalSpectralEnergy ξ ζ := by @@ -2778,7 +2774,7 @@ private theorem dSVUniformDensitySpectralAtomDiscrepancy_le apply Finset.sum_congr rfl intro j _ rw [sq_abs] - ring + ac_rfl have exact_mass : (∑ ij : Fin d × Fin d, weight ij * g ij ^ 2) = dSVUniformDensitySchmidtSumMass ξ ζ := by @@ -2789,7 +2785,7 @@ private theorem dSVUniformDensitySpectralAtomDiscrepancy_le apply Finset.sum_congr rfl intro j _ dsimp [weight, g, F, G, hF, hG, σ, μ] - ring + ac_rfl rw [exact_l1, exact_energy, exact_mass] at cauchy have target_energy := targetCanonicalSpectralEnergy_le ξ ζ have sum_mass := dSVUniformDensitySchmidtSumMass_le_four ξ ζ @@ -2801,13 +2797,13 @@ private theorem dSVUniformDensitySpectralAtomDiscrepancy_le · positivity · have square_two : Real.sqrt (2 : ℝ) ^ 2 = 2 := Real.sq_sqrt (by norm_num) - nlinarith [sq_nonneg ‖ξ.val - ζ.val‖] + nlinarith only [target_energy, square_two] have second : Real.sqrt (dSVUniformDensitySchmidtSumMass ξ ζ) ≤ 2 := by apply Real.sqrt_le_iff.mpr constructor · norm_num - · linarith + · linarith only [sum_mass] calc _ ≤ Real.sqrt (targetCanonicalSpectralEnergy ξ ζ) * Real.sqrt (dSVUniformDensitySchmidtSumMass ξ ζ) := @@ -2815,7 +2811,7 @@ private theorem dSVUniformDensitySpectralAtomDiscrepancy_le _ ≤ (Real.sqrt 2 * ‖ξ.val - ζ.val‖) * 2 := mul_le_mul first second (Real.sqrt_nonneg _) (by positivity) - _ = 2 * Real.sqrt 2 * ‖ξ.val - ζ.val‖ := by ring + _ = 2 * Real.sqrt 2 * ‖ξ.val - ζ.val‖ := by ac_rfl end @@ -3218,8 +3214,6 @@ private theorem sharedPermutation_disagreement_probability_le_two_mul_tv rank left right hleft hright _ = 2 * markedTotalVariation left right := by unfold markedTotalVariation - have hcard : (left.card : ℝ) ≠ 0 := by - exact_mod_cast (Finset.card_ne_zero.mpr hleft) field_simp section RationalMarks @@ -3374,7 +3368,7 @@ theorem centered_log_lower_of_one_le {x : ℝ} (hx : 1 ≤ x) : exact div_nonneg (sub_nonneg.mpr hx) hden.le have ht1 : t < 1 := by apply (div_lt_one hden).mpr - linarith + linarith only [] have hratio : (1 + t) / (1 - t) = x := by dsimp [t] field_simp @@ -3387,7 +3381,7 @@ theorem centered_log_lower_of_one_le {x : ℝ} (hx : 1 ≤ x) : dsimp [t] at hseries calc 2 * (x - 1) / (x + 1) = 2 * ((x - 1) / (x + 1)) := by ring - _ ≤ Real.log x := by linarith + _ ≤ Real.log x := by linarith only [hseries] theorem centered_log_upper_of_le_one {x : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) : @@ -3403,7 +3397,7 @@ theorem centered_log_upper_of_le_one ring rw [hratio, Real.log_div (by norm_num : (1 : ℝ) ≠ 0) hx0.ne', Real.log_one] at h - linarith + linarith only [h] private def pinskerScalarGap (x : ℝ) : ℝ := InformationTheory.klFun x - 3 * (x - 1) ^ 2 / (2 * (x + 2)) @@ -3436,9 +3430,9 @@ private theorem hasDerivAt_pinskerScalarGap {x : ℝ} (hx : 0 < x) : theorem pinsker_rational_coefficient_le {x : ℝ} (hx : 0 < x) : 3 * (x + 5) / (2 * (x + 2) ^ 2) ≤ 2 / (x + 1) := by have hleft : 0 < 2 * (x + 2) ^ 2 := by positivity - have hright : 0 < x + 1 := by linarith + have hright : 0 < x + 1 := by linarith only [hx] apply (div_le_div_iff₀ hleft hright).mpr - linarith [sq_nonneg (x - 1)] + linarith only [sq_nonneg (x - 1)] theorem pinskerScalarGap_derivative_nonneg {x : ℝ} (hx : 1 ≤ x) : @@ -3457,7 +3451,7 @@ theorem pinskerScalarGap_derivative_nonneg _ ≤ (x - 1) * (2 / (x + 1)) := hscaled _ = 2 * (x - 1) / (x + 1) := by ring have hlog := centered_log_lower_of_one_le hx - linarith + linarith only [hrational, hlog] theorem pinskerScalarGap_derivative_nonpos {x : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) : @@ -3474,7 +3468,7 @@ theorem pinskerScalarGap_derivative_nonpos _ ≤ (x - 1) * (3 * (x + 5) / (2 * (x + 2) ^ 2)) := hscaled _ = 3 * (x - 1) * (x + 5) / (2 * (x + 2) ^ 2) := by ring have hlog := centered_log_upper_of_le_one hx0 hx1 - linarith + linarith only [hrational, hlog] private theorem pinskerScalarGap_nonneg {x : ℝ} (hx : 0 ≤ x) : 0 ≤ pinskerScalarGap x := by @@ -3489,7 +3483,7 @@ private theorem pinskerScalarGap_nonneg {x : ℝ} (hx : 0 ≤ x) : intro y hy have hypos : 0 < y := by have hyone := (Set.mem_Icc.mp hy).1 - linarith + linarith only [hyone] exact (hasDerivAt_pinskerScalarGap hypos).continuousAt.continuousWithinAt have hmonotone : MonotoneOn pinskerScalarGap (Set.Icc 1 x) := by apply monotoneOn_of_hasDerivWithinAt_nonneg @@ -3498,7 +3492,7 @@ private theorem pinskerScalarGap_nonneg {x : ℝ} (hx : 0 ≤ x) : have hymem : y ∈ Set.Icc (1 : ℝ) x := interior_subset hy have hypos : 0 < y := by have hyone := (Set.mem_Icc.mp hymem).1 - linarith + linarith only [hyone] exact (hasDerivAt_pinskerScalarGap hypos).hasDerivWithinAt · intro y hy have hymem : y ∈ Set.Icc (1 : ℝ) x := interior_subset hy @@ -3645,11 +3639,8 @@ theorem finite_pinsker _ = 2 * finiteRelativeEntropy p q := by unfold finiteRelativeEntropy rw [Finset.mul_sum] - have hmain : - (∑ i, |p i - q i|) ^ 2 ≤ 2 * finiteRelativeEntropy p q := - hcauchy.trans hsum unfold finiteTotalVariation - linarith + linarith only [hcauchy, hsum] theorem sum_over_positive_reference_support {ι : Type*} [Fintype ι] @@ -3833,7 +3824,7 @@ private theorem distributionFloorProbability_error_lt (denominator : ℝ)) * (denominator : ℝ) = p i * (denominator : ℝ) - Nat.floor (p i * (denominator : ℝ)) := by field_simp - _ < 1 := by linarith + _ < 1 := by linarith only [hupper] omit [DecidableEq ι] in theorem distributionFloorNumerator_sum_le @@ -3880,8 +3871,6 @@ private theorem distributionFloorResidual_probability_eq_sum ∑ i, (p i - distributionFloorProbability denominator p i) := by have hfloor := distributionFloorNumerator_sum_le denominator p hp normalized - have hden : (denominator : ℝ) ≠ 0 := by - exact_mod_cast (Nat.ne_of_gt positive) unfold distributionFloorResidual distributionFloorProbability rw [Nat.cast_sub hfloor, Nat.cast_sum, Finset.sum_sub_distrib, normalized, ← Finset.sum_div] @@ -4422,7 +4411,7 @@ private theorem rationalMarked_markedTotalVariation_eq 2 * ∑ i : ι, (min (left i) (right i) : ℝ) := by have hLreal : (L.card : ℝ) = denominator := by exact_mod_cast hL have hRreal : (R.card : ℝ) = denominator := by exact_mod_cast hR - linarith + linarith only [hI, hunion, hleft_difference, hright_difference, hLreal, hRreal] have hpointwise : ∀ i : ι, |(left i : ℝ) / denominator - (right i : ℝ) / denominator| = @@ -4584,9 +4573,7 @@ private theorem dSVUniformLeftDensityConjugateSwapVector_norm ∑ i : Fin d, ∑ j : Fin d, ‖z (i, j)‖ ^ 2 simp_rw [norm_star] rw [Finset.sum_comm] - nlinarith [norm_nonneg - (dSVUniformLeftDensityConjugateSwapVector z), - norm_nonneg z] + exact (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp squares private theorem dSVUniformLeftDensityConjugateSwapVector_distance {d : ℕ} (z w : EuclideanSpace ℂ (Fin d × Fin d)) : @@ -4706,8 +4693,6 @@ theorem dSVUniformDensityThresholdGrid_apply {N : ℕ} (positive : 0 < N) (k : Fin N) : dSVUniformDensityThresholdGrid N k = ((k.val : ℝ) + 1) / (N : ℝ) := by - have nonzero : (N : ℝ) ≠ 0 := by - exact_mod_cast (Nat.ne_of_gt positive) unfold dSVUniformDensityThresholdGrid finiteUniformThresholdGrid field_simp @@ -4799,7 +4784,7 @@ theorem dSVUniformDensityThresholdMismatch_le |alice - bob| + 1 / (N : ℝ) := by classical have window : - (1 / (N : ℝ)) < 1 + 1 / (N : ℝ) := by linarith + (1 / (N : ℝ)) < 1 + 1 / (N : ℝ) := by linarith only [] calc dSVUniformDensityThresholdMismatch N alice bob ≤ finiteUniformThresholdCrossing @@ -5005,9 +4990,9 @@ theorem normalizeOrDefault_sub_le rw [hsplit] exact norm_add_le _ _ _ = ‖u - v‖ + |‖v‖ - ‖u‖| := by rw [hsecond] - _ ≤ 2 * ‖u - v‖ := by linarith + _ ≤ 2 * ‖u - v‖ := by linarith only [hreverse] change ‖u₀ - v₀‖ ≤ 2 * ‖u - v‖ / ‖u‖ - exact (le_div_iff₀ hupos).mpr (by linarith) + exact (le_div_iff₀ hupos).mpr (by linarith only [hbound]) end @@ -5041,7 +5026,7 @@ theorem dSVCanonicalFailurePrefix_eq_zero_of_rank_zero simpa only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, norm_eq_zero, zero, CharP.cast_eq_zero] using dSVCanonicalFailurePrefix_norm_sq rank have normzero : ‖dSVCanonicalFailurePrefix rank‖ = 0 := by - nlinarith [norm_nonneg (dSVCanonicalFailurePrefix rank)] + exact sq_eq_zero_iff.mp squared exact norm_eq_zero.mp normzero theorem dSVCanonicalFailurePrefix_norm_eq_sqrt @@ -5050,8 +5035,7 @@ theorem dSVCanonicalFailurePrefix_norm_eq_sqrt Real.sqrt (rank.val : ℝ) := by have squared := dSVCanonicalFailurePrefix_norm_sq rank have root := Real.sq_sqrt (by positivity : 0 ≤ (rank.val : ℝ)) - nlinarith [norm_nonneg (dSVCanonicalFailurePrefix rank), - Real.sqrt_nonneg (rank.val : ℝ)] + exact (sq_eq_sq₀ (norm_nonneg _) (Real.sqrt_nonneg _)).mp (squared.trans root.symm) end @@ -5379,10 +5363,10 @@ theorem dSVUniformDensityCompletePureHistory_raw_norm _ = (((N * d) ^ (L + 1) : ℕ) : ℝ) := by rw [hsquare] push_cast - ring + ac_rfl change ‖whole‖ = ‖single‖ ^ (L + 1) - nlinarith [norm_nonneg whole, - pow_nonneg (norm_nonneg single) (L + 1)] + exact (sq_eq_sq₀ (norm_nonneg whole) (pow_nonneg (norm_nonneg single) _)).mp + (hwhole.trans hpower.symm) theorem dSVUniformDensityCompletePureHistory_zeroFlag_apply (N d L : ℕ) @@ -5791,11 +5775,10 @@ theorem finitePurificationMatrix_gram_apply F M positive hM a r i let v := ensemblePurificationSubspaceEntry F M positive hM a r j - have hisometry := b.repr.inner_map_map u v change (∑ k, star (b.repr u k) * b.repr v k) = inner ℂ u v - rw [← hisometry, EuclideanSpace.inner_eq_star_dotProduct] - simp only [RCLike.star_def, mul_comm, dotProduct, Pi.star_apply] + simpa only [OrthonormalBasis.repr_apply_apply, RCLike.star_def, inner_conj_symm] + using b.sum_inner_mul_inner u v theorem ensemblePurificationSubspaceEntry_inner_eq_integral {ι d : Type*} [Fintype d] [DecidableEq d] @@ -5932,14 +5915,13 @@ private theorem finitePurificationMatrix_difference_gram_apply F M positive hM a r j let v₀ := meanPurificationSubspaceEntry F M positive hM r j - have hisometry := b.repr.inner_map_map (u - u₀) (v - v₀) change (∑ k, star (b.repr u k - b.repr u₀ k) * (b.repr v k - b.repr v₀ k)) = inner ℂ (u - u₀) (v - v₀) - rw [← hisometry, EuclideanSpace.inner_eq_star_dotProduct] - simp only [star_sub, RCLike.star_def, mul_comm, dotProduct, map_sub, PiLp.sub_apply, - WithLp.ofLp_sub, Pi.star_apply, Pi.sub_apply] + simpa only [OrthonormalBasis.repr_apply_apply, inner_sub_left, inner_sub_right, + star_sub, RCLike.star_def, inner_conj_symm] + using b.sum_inner_mul_inner (u - u₀) (v - v₀) private theorem purificationSubspaceEntry_difference_inner_eq_integral {ι d : Type*} [Fintype d] [DecidableEq d] @@ -6223,7 +6205,8 @@ theorem strategyPurificationVector_norm (Matrix.trace S.state.matrix).re rw [spectralSupportSqrt_sq] _ = 1 := by rw [S.state.trace_one]; norm_num - nlinarith [norm_nonneg (strategyPurificationVector S)] + exact (sq_eq_sq₀ (norm_nonneg _) zero_le_one).mp (by + simpa only [one_pow] using h_sq) theorem reindexedMatrixQuadratic {d e : Type*} [Fintype d] [Fintype e] @@ -6452,8 +6435,7 @@ theorem dSVUniformDensityMixedProtocolLocalAction_norm simp only [quadraticExpectation, map_one, one_apply_eq_self, inner_self_eq_norm_sq_to_K, coe_algebraMap, ← ofReal_pow, ofReal_re] change ‖toLp 2 (M.mulVec (ofLp z))‖ = ‖z‖ - nlinarith [norm_nonneg (toLp 2 (M.mulVec (ofLp z))), - norm_nonneg z] + exact (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp squared end @@ -7052,14 +7034,13 @@ theorem dSVUniformDensityGridPrefix_density_sub_lt (N : ℝ) = a * (N : ℝ) - (Nat.floor (a * (N : ℝ)) : ℝ) := by field_simp - _ < 1 := by linarith + _ < 1 := by linarith only [floor] theorem dSVUniformDensityGridPrefix_density_sub_le {N : ℕ} (positive : 0 < N) {a : ℝ} (nonnegative : 0 ≤ a) (bounded : a ≤ 1) : a - 1 / (N : ℝ) ≤ dSVUniformDensityGridPrefix N a := by - linarith [dSVUniformDensityGridPrefix_density_sub_lt - positive nonnegative bounded] + linarith only [dSVUniformDensityGridPrefix_density_sub_lt positive nonnegative bounded] /-- The total probability mass of DSV density rational left projective diagonal. -/ def dSVDensityRationalLeftProjectiveDiagonalMass @@ -7093,9 +7074,9 @@ theorem dSVRationalSoftPass_ge_density_div_width_add_one a / (w + 1) ≤ dSVRationalSoftPass w a := by unfold dSVRationalSoftPass have denominator : 0 < a + w := by linarith - have wider : 0 < w + 1 := by linarith + have wider : 0 < w + 1 := by linarith only [width] apply (div_le_div_iff₀ wider denominator).mpr - nlinarith + nlinarith only [nonnegative, bounded] theorem dSVDensityRationalLeftProjectiveDiagonalMass_lower {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) diff --git a/LeanPool/QuantumParallelRepetition/Part03.lean b/LeanPool/QuantumParallelRepetition/Part03.lean index 7dda564628..564d41a75a 100644 --- a/LeanPool/QuantumParallelRepetition/Part03.lean +++ b/LeanPool/QuantumParallelRepetition/Part03.lean @@ -280,10 +280,6 @@ theorem dSVDensityRationalPhysicalDiagonalBornSuccess_eq grid dimension w ξ = dSVDensityRationalLeftProjectiveDiagonalMass w N ξ / (d : ℝ) := by - have d_nonzero : (d : ℝ) ≠ 0 := by - exact_mod_cast (Nat.ne_of_gt dimension) - have n_nonzero : (N : ℝ) ≠ 0 := by - exact_mod_cast (Nat.ne_of_gt grid) unfold dSVDensityRationalPhysicalDiagonalBornSuccess dSVDensityRationalPhysicalGlobalPOVM rw [dSVUniformDensityThresholdShared_diagonalBorn_eq @@ -318,10 +314,6 @@ theorem dSVDensityRationalPhysicalProjectorCrossHazard_eq dSVDensityRationalPhysicalProjectorCrossHazard N w ξ ζ = dSVDensityRationalLeftProjectiveThresholdAtomMismatch w N ξ ζ / (d : ℝ) := by - have d_nonzero : (d : ℝ) ≠ 0 := by - exact_mod_cast (Nat.ne_of_gt dimension) - have n_nonzero : (N : ℝ) ≠ 0 := by - exact_mod_cast (Nat.ne_of_gt grid) unfold dSVDensityRationalPhysicalProjectorCrossHazard calc (∑ k : Fin N, @@ -613,18 +605,18 @@ theorem dSVDensityRationalGridPrefix_nonneg theorem dSVDensityRationalSoftPass_rescaled_le_density {w a : ℝ} (width : 0 < w) (nonnegative : 0 ≤ a) : w * dSVRationalSoftPass w a ≤ a := by - have denominator : 0 < a + w := by linarith + have denominator : 0 < a + w := by linarith only [width, nonnegative] unfold dSVRationalSoftPass calc w * (a / (a + w)) = w * a / (a + w) := by ring _ ≤ a := (div_le_iff₀ denominator).mpr (by - linarith [sq_nonneg a]) + linarith only [sq_nonneg a]) theorem dSVDensityRationalSoftPass_density_defect_le {w a : ℝ} (width : 0 < w) (nonnegative : 0 ≤ a) (bounded : a ≤ 1) : a - w * dSVRationalSoftPass w a ≤ a / w := by - have denominator : 0 < a + w := by linarith + have denominator : 0 < a + w := by linarith only [width, nonnegative] calc a - w * dSVRationalSoftPass w a = a ^ 2 / (a + w) := by @@ -633,8 +625,8 @@ theorem dSVDensityRationalSoftPass_density_defect_le ring _ ≤ a / w := by apply (div_le_div_iff₀ denominator width).mpr - linarith [mul_nonneg (mul_nonneg nonnegative width.le) - (sub_nonneg.mpr bounded), sq_nonneg a] + linarith only [mul_nonneg (mul_nonneg nonnegative width.le) (sub_nonneg.mpr bounded), + sq_nonneg a] theorem dSVDensityRationalGrid_rescaled_le_density {N : ℕ} {w a : ℝ} (width : 0 < w) (grid : 0 < N) @@ -831,9 +823,7 @@ theorem dSVDensityRationalCanonicalAcceptedTarget_distance_le dSVDensityRationalCanonicalAcceptedTarget_distance_sq_le width grid ξ have exact_sqrt := Real.sq_sqrt nonnegative - nlinarith [norm_nonneg - (ξ.val - dSVDensityRationalCanonicalAcceptedTarget w N ξ), - Real.sqrt_nonneg (1 / w + (d : ℝ) * w / (N : ℝ))] + nlinarith only [squared, exact_sqrt, Real.sqrt_nonneg (1 / w + (d : ℝ) * w / (N : ℝ))] theorem dSVDensityRationalCanonicalAcceptedTarget_ne_zero {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) @@ -848,7 +838,7 @@ theorem dSVDensityRationalCanonicalAcceptedTarget_ne_zero have lower := dSVDensityRationalLeftProjectiveDiagonalMass_lower width grid ξ - nlinarith + nlinarith only [actual, width, fine, lower] /-- Normalize the canonical accepted target vector. -/ def dSVDensityRationalCanonicalNormalizedTarget @@ -897,7 +887,7 @@ private theorem dSVDensityRationalCanonicalNormalizedTarget_distance_le norm_add_le _ _ _ ≤ 2 * ‖ξ.val - v‖ := by rw [movement] - linarith + linarith only [reverse] _ ≤ 2 * Real.sqrt (1 / w + (d : ℝ) * w / (N : ℝ)) := by gcongr exact dSVDensityRationalCanonicalAcceptedTarget_distance_le @@ -937,14 +927,13 @@ theorem dSVDensityRationalLargeWidthDiagonalMass_half (ξ : BipartiteUnitVector d) : 1 / (2 * (w + 1)) ≤ dSVDensityRationalLeftProjectiveDiagonalMass w N ξ := by - have denominator : 0 < w + 1 := by linarith have arithmetic : 1 / (2 * (w + 1)) ≤ 1 / (w + 1) - (d : ℝ) / N := by have identity : 1 / (w + 1) - 1 / (2 * (w + 1)) = 1 / (2 * (w + 1)) := by field_simp; ring - linarith + linarith only [fine, identity] exact arithmetic.trans (dSVDensityRationalLeftProjectiveDiagonalMass_lower width grid ξ) @@ -1002,7 +991,7 @@ theorem have floor_scaled : 1 ≤ 2 * (w + 1) * M := by have denominator : 0 < 2 * (w + 1) := by positivity have crossed := (div_le_iff₀ denominator).mp mass_floor - linarith + linarith only [crossed] change dSVDensityRationalLeftProjectiveThresholdAtomMismatch w N ξ ζ ≤ (2 * (w + 1) * D) * M @@ -1012,7 +1001,7 @@ theorem _ ≤ D * (2 * (w + 1) * M) := by linarith [mul_nonneg defect_nonnegative (show 0 ≤ 2 * (w + 1) * M - 1 by linarith)] - _ = (2 * (w + 1) * D) * M := by ring + _ = (2 * (w + 1) * D) * M := by ac_rfl theorem dSVDensityRationalLargeWidthRelativeMismatch_le_targetDistance @@ -1032,7 +1021,7 @@ theorem have denominator : 0 < w := width have ratio : (w + 1) / w ≤ 2 := by apply (div_le_iff₀ denominator).mpr - linarith + linarith only [large] calc dSVDensityRationalLeftProjectiveThresholdAtomMismatch w N ξ ζ / @@ -1076,10 +1065,10 @@ theorem dSVDensityRationalLargeWidth_exists_fine_grid have crossed := (div_lt_iff₀ denominator).mp large have small : (d : ℝ) / N < ε / (2 * (w + 1)) := by apply (div_lt_iff₀ real_grid).mpr - linarith + linarith only [crossed] have positive : 0 < 2 * (w + 1) := by positivity have scaled := (lt_div_iff₀ positive).mp small - linarith + linarith only [scaled] theorem dSVDensityRationalLargeWidth_exists_sourceUniformParameters (d : ℕ) (dimension : 0 < d) @@ -1107,16 +1096,16 @@ theorem dSVDensityRationalLargeWidth_exists_sourceUniformParameters have fine : (d : ℝ) / N ≤ 1 / (2 * (w + 1)) := by have denominator : 0 < 2 * (w + 1) := by positivity apply (le_div_iff₀ denominator).mpr - linarith + linarith only [small, budget] have inverse : 1 / w = ε := by dsimp [w] field_simp have rounding : 1 / w + w * ((d : ℝ) / N) ≤ 3 * ε / 2 := by have grid_cost : w * ((d : ℝ) / N) ≤ ε / 2 := by have weight : 0 ≤ (d : ℝ) / N := by positivity - linarith + linarith only [budget, weight] rw [inverse] - linarith + linarith only [grid_cost] refine ⟨w, N, large, grid, budget, rounding, ?_, ?_⟩ · intro ξ exact dSVDensityRationalLargeWidthDiagonalMass_pos @@ -1764,7 +1753,7 @@ private theorem dSVDensityRationalMixedSpectralAtomBlock_trace_eq intro i _ apply Finset.sum_congr rfl intro j _ - split_ifs <;> simp [spectralAtomOverlap] + split_ifs <;> simp only [spectralAtomOverlap, trace_zero, zero_re] end @@ -1996,7 +1985,7 @@ theorem dSVDensityRationalMixedAcceptedPrefix_norm_sq rw [Finset.mul_sum] apply Finset.sum_congr rfl intro k _ - split_ifs <;> simp + split_ifs <;> simp only [mul_one, mul_zero] _ = _ := by rw [counted] /-- @@ -2403,10 +2392,7 @@ theorem tensorEmbezzlementTarget_sub_norm ← EuclideanSpace.norm_sq_eq, ← EuclideanSpace.norm_sq_eq, embezzlementState_norm n positive] ring - nlinarith [norm_nonneg - (tensorEmbezzlementTarget (n := n) ξ - - tensorEmbezzlementTarget (n := n) ζ), - norm_nonneg (ξ.val - ζ.val)] + exact (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp squares end @@ -2670,17 +2656,10 @@ theorem dSVDensityRationalPublicBucketLocalHarmonicCleanup_sq (Nat.mul_pos dimension positive)] norm_num simp only [ite_eq_right same, mul_one] - nlinarith [ - norm_nonneg - (localUnitaryAction - (A (phase, bucket phase r)) - (B (phase, bucket phase s)) - (tensorEmbezzlementTarget (n := n) (work r)) - - embezzlementState (N * n)), - sq_nonneg ε, - sq_nonneg - ‖(work r).val - - (work (representative phase (bucket phase r))).val‖] + nlinarith only [bound, precision, + norm_nonneg (localUnitaryAction + (A (phase, bucket phase r)) (B (phase, bucket phase s)) + (tensorEmbezzlementTarget (n := n) (work r)) - embezzlementState (N * n))] theorem dSVDensityRationalPublicBucketCanonicalPrefixCleanup_sq {Ω I : Type*} [DecidableEq I] {N : ℕ} (grid : 0 < N) @@ -3083,10 +3062,10 @@ theorem dSVDensityRationalPublicLogRankBucket_log_sub_lt (Real.log ((max 1 s.val : ℕ) : ℝ)) with ordered | ordered · rw [abs_of_nonpos (sub_nonpos.mpr ordered)] have integer_order := (abs_lt.mp bucket_bounds).1 - linarith [rank_bounds.1, other_bounds.2] + linarith only [rank_bounds, other_bounds, integer_order] · rw [abs_of_nonneg (sub_nonneg.mpr ordered)] have integer_order := (abs_lt.mp bucket_bounds).2 - linarith [rank_bounds.2, other_bounds.1] + linarith only [rank_bounds, other_bounds, integer_order] /-- The nonzero ranks assigned to the given logarithmic bucket and public phase. -/ def dSVDensityRationalPublicLogRankBucketFiber @@ -3777,8 +3756,7 @@ private theorem dSVDensityRationalPublicLogPhasePureSource_norm dSVUniformDensityThresholdWholeHistorySharedState_norm grid dimension L] norm_num - nlinarith [norm_nonneg - (dSVDensityRationalPublicLogPhasePureSource B N d L)] + nlinarith only [squared, norm_nonneg (dSVDensityRationalPublicLogPhasePureSource B N d L)] /-- Adjoin the harmonic embezzlement state to the public-phase history source. -/ def dSVDensityRationalPublicLogPhaseHarmonicPureSource @@ -3826,9 +3804,8 @@ private theorem dSVDensityRationalPublicLogPhaseHarmonicPureSource_norm phases grid dimension, embezzlementState_norm m harmonic] norm_num - nlinarith [norm_nonneg - (dSVDensityRationalPublicLogPhaseHarmonicPureSource - B N d L m)] + nlinarith only [squared, + norm_nonneg (dSVDensityRationalPublicLogPhaseHarmonicPureSource B N d L m)] /-- The public-phase label paired with the residual whole-history catalyst index. -/ abbrev DSVDensityRationalPublicLogPhaseCatalystIndex @@ -4669,9 +4646,8 @@ theorem have stage (k : ℕ) : success k + asynchronous k = 1 - continuation k := by dsimp [continuation, success, asynchronous] - linarith [ - dSVDensityRationalHeterogeneousPhysicalStage_partition - grid dimension width schedule ξ ζ k] + linarith only [ + dSVDensityRationalHeterogeneousPhysicalStage_partition grid dimension width schedule ξ ζ k] have escape := dSVHeterogeneousRealStopping_escape_identity continuation L @@ -4849,7 +4825,7 @@ private theorem N width schedule ξ ζ k * x) (dSVDensityRationalHeterogeneousPhysicalStageAsynchronous_eq_escape_mul_ratio N width schedule ξ ζ k) - _ = _ := by ring + _ = _ := by ac_rfl theorem dSVDensityRationalHeterogeneousPhysicalStageDiagonalSuccess_lower @@ -4979,7 +4955,7 @@ private theorem 2 * (W + 1) * ((d : ℝ) / N) := by have scale := upper (schedule k) have grid_cost : 0 ≤ (d : ℝ) / N := by positivity - linarith [mul_nonneg grid_cost (sub_nonneg.mpr scale)] + linarith only [mul_nonneg grid_cost (sub_nonneg.mpr scale)] theorem dSVDensityRationalHeterogeneousPhysicalStoppedEscape_budget {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) @@ -5011,7 +4987,7 @@ theorem dSVDensityRationalHeterogeneousPhysicalStoppedEscape_budget dSVDensityRationalHeterogeneousPhysicalStage_partition grid dimension width schedule ξ ζ k dsimp [continuation, escape] - linarith + linarith only [actual] simpa only [dSVDensityRationalHeterogeneousPhysicalSurvival, ge_iff_le] using dSVHeterogeneousRealStopping_escape_budget continuation escape continuation_nonnegative stage L @@ -5102,8 +5078,7 @@ theorem N width schedule ξ ζ k)) * bound := by rw [Finset.sum_mul] _ ≤ bound := by - linarith [mul_nonneg bound_nonnegative - (sub_nonneg.mpr escape_budget)] + linarith only [mul_nonneg bound_nonnegative (sub_nonneg.mpr escape_budget)] /-- The error rate associated with DSV density rational heterogeneous physical uniform escape. -/ def dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate @@ -5133,7 +5108,7 @@ theorem positivity unfold dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate apply (div_le_div_iff₀ denominator (by norm_num : (0 : ℝ) < 2)).mpr - linarith [mul_nonneg W_nonnegative real_dimension.le] + linarith only [dimension_one, mul_nonneg W_nonnegative real_dimension.le] theorem dSVDensityRationalHeterogeneousPhysicalStageDiagonalSuccess_ge_uniform @@ -5164,8 +5139,7 @@ theorem d W = 1 / (2 * (W + 1) * (d : ℝ)) := rfl _ ≤ 1 / (2 * (width (schedule k) + 1) * (d : ℝ)) := by apply (div_le_div_iff₀ wide_positive stage_positive).mpr - linarith [mul_nonneg real_dimension.le - (sub_nonneg.mpr width_bound)] + linarith only [mul_nonneg real_dimension.le (sub_nonneg.mpr width_bound)] _ ≤ dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension (width (schedule k)) ξ := dSVDensityRationalHeterogeneousPhysicalStageDiagonalSuccess_lower @@ -5476,7 +5450,7 @@ private theorem rightSpectralBornWeight_moment apply Finset.sum_congr rfl intro i _ unfold rightSpectralBornWeight - ring + ac_rfl _ = bornTracePairing ρ.matrix F G := h.symm private theorem rightSpectralBornWeight_entropy @@ -5508,7 +5482,7 @@ private theorem rightSpectralBornWeight_entropy apply Finset.sum_congr rfl intro i _ unfold rightSpectralBornWeight - ring + ac_rfl private theorem rightSpectralBornWeight_negEntropy {dA dB : Type*} @@ -5547,7 +5521,7 @@ theorem bornTracePairing_le_one_one bornTracePairing ρ.matrix F (1 : Matrix dB dB ℂ) := by simp only [map_sub, LinearMap.sub_apply] rw [hdiff, bornTracePairing_one_one] at hpositive - linarith + linarith only [hpositive] theorem matrixLogEntropy_born_lower_bound_right {dA dB : Type*} @@ -5851,7 +5825,7 @@ theorem bornTracePairing_contractions_le_one simp only [map_sub, LinearMap.sub_apply] rw [hdiff] at hpositive have hone := bornTracePairing_one_le_one ρ G hGcomplement - linarith + linarith only [hpositive, hone] theorem fullHistoryAtomBornMass_le_one (G : Game X Y A B) (n : ℕ) @@ -5901,7 +5875,7 @@ theorem fullHistoryAtomCountingWeight_sum_le nsmul_eq_mul, Nat.cast_pow, fullHistoryAnswerCount, mul_sum, mul_assoc] _ = fullHistoryAnswerCount (A := A) (B := B) D := by rw [fullHistoryWeight_sum G D L] - ring + ac_rfl theorem fullHistoryAtomBornMass_sum (G : Game X Y A B) (n : ℕ) @@ -6003,9 +5977,9 @@ theorem fullHistoryAliceEntropyPotential_lower_bound (fullHistoryBobFilter G n S D L h β) (fullHistoryBobFilter_posSemidef G n S D L h β) (fullHistoryBobFilter_complement_posSemidef G n S D L h β) - linarith [mul_le_mul_of_nonneg_left hlocal hw] + linarith only [mul_le_mul_of_nonneg_left hlocal hw] have hscalar := fullHistoryAtomEntropy_le G n S D L hL hp - linarith + linarith only [hpoint, hscalar] end @@ -6361,7 +6335,7 @@ theorem fullCoordinateOldHistory_weight rw [fullHistoryRemaining_prod_split D L i hiD hiL] simp_rw [hold] simp only [univ_eq_attach, fullCoordinateOldHistory, ↓reduceDIte] - ring + ac_rfl theorem fullCoordinateNewHistory_weight (G : Game X Y A B) {n : ℕ} @@ -6392,7 +6366,7 @@ theorem fullCoordinateNewHistory_weight rw [finsetSubtype_prod_insert L i hiL] simp_rw [hnew] simp only [univ_eq_attach, fullCoordinateNewHistory, ↓reduceDIte] - ring + ac_rfl end CoordinateWeights @@ -6432,14 +6406,13 @@ theorem finitePurificationMatrix_pair_difference_gram_apply let u₀ := ensemblePurificationSubspaceEntry F M positive hM b r i let v := ensemblePurificationSubspaceEntry F M positive hM a r j let v₀ := ensemblePurificationSubspaceEntry F M positive hM b r j - have hisometry := basis.repr.inner_map_map (u - u₀) (v - v₀) change (∑ k, star (basis.repr u k - basis.repr u₀ k) * (basis.repr v k - basis.repr v₀ k)) = inner ℂ (u - u₀) (v - v₀) - rw [← hisometry, EuclideanSpace.inner_eq_star_dotProduct] - simp only [star_sub, RCLike.star_def, mul_comm, dotProduct, map_sub, PiLp.sub_apply, - WithLp.ofLp_sub, Pi.star_apply, Pi.sub_apply] + simpa only [OrthonormalBasis.repr_apply_apply, inner_sub_left, inner_sub_right, + star_sub, RCLike.star_def, inner_conj_symm] + using basis.sum_inner_mul_inner (u - u₀) (v - v₀) theorem ensemblePurificationSubspaceEntry_pair_difference_inner_eq_integral {ι d : Type*} [Fintype d] [DecidableEq d] @@ -7325,7 +7298,7 @@ theorem fullCoordinateWeightedOldSum intro y _ rw [fullCoordinateOldHistory_weight G D L i hiD hiL r y, fullCoordinateOldHistory_winIndicator_eq G D L i r y α β] - ring + ac_rfl theorem fullCoordinateWeightedNewSum (G : Game X Y A B) {n : ℕ} @@ -7379,7 +7352,7 @@ theorem fullCoordinateWeightedNewSum intro x _ rw [fullCoordinateNewHistory_weight G D L i hiL r x, fullCoordinateNewHistory_winIndicator_eq G D L i r x α β] - ring + ac_rfl /-- The information increment contributed by full coordinate alice total entropy. -/ def fullCoordinateAliceTotalEntropyIncrement diff --git a/LeanPool/QuantumParallelRepetition/Part04.lean b/LeanPool/QuantumParallelRepetition/Part04.lean index 06c04e4d26..0c58ad5520 100644 --- a/LeanPool/QuantumParallelRepetition/Part04.lean +++ b/LeanPool/QuantumParallelRepetition/Part04.lean @@ -207,7 +207,7 @@ theorem fin_sum_successive_sub rw [Finset.sum_sub_distrib] have hfirst := Fin.sum_univ_succ f have hlast := Fin.sum_univ_castSucc f - linarith + linarith only [hfirst, hlast] section ActualEntropyBudgets @@ -296,7 +296,7 @@ private theorem sourcePermutationAliceEntropyIncrement_sum_le G n S D (Finset.univ \ D) have hfirst := fullHistoryAliceEntropyPotential_lower_bound G n S D ∅ (Finset.empty_subset _) hp - linarith + linarith only [hlast, hfirst] private def sourceUniformPermutationAverage {n : ℕ} (D : Finset (Fin n)) @@ -603,7 +603,7 @@ theorem exactUniform_sum_mul (∑ _t : T, value * (1 / (Fintype.card T : ℝ))) = value := by rw [← Finset.mul_sum, exactUniform_sum positive] - ring + ac_rfl theorem exactPrefixUniform_sum_mul (m : ℕ) (value : ℝ) : @@ -766,7 +766,7 @@ theorem commonFinitePurification_weighted_left_variation_le finitePurificationMatrix F anchor positive hanchor meanIndex))) (KB.conjTranspose * KB) at hnonneg rw [hsum] at hnonneg - linarith + linarith only [positive, hanchor, hnonneg] theorem commonFinitePurification_weighted_right_variation_le {X Y A B ι κ eA : Type*} @@ -828,7 +828,7 @@ theorem commonFinitePurification_weighted_right_variation_le intro b _ rw [finiteLocalPurificationVector_sub_right_norm_sq] rw [map_sub, hsum] at hnonneg - linarith + linarith only [positive, hanchor, hnonneg] end @@ -2074,8 +2074,7 @@ theorem exactPaddedVector_norm simp only [exactPaddedVector, EuclideanSpace.norm_sq_eq, Fintype.sum_prod_type, Fintype.sum_sum_type, univ_unique, PUnit.default_eq_unit, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, sum_const_zero, zero_add, add_zero] - nlinarith [norm_nonneg (exactPaddedVector G n S D r z), - norm_nonneg z] + exact (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp hsquare theorem exactPaddedVector_sub (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) @@ -2372,8 +2371,8 @@ theorem exactFiberQuestionWeight_rectangle D seed history y ys <;> by_cases hb' : exactBobQuestionCompatible D seed history y ys' <;> - simp [exactFiberQuestionWeight, - ha, ha', hb, hb'] + simp only [exactFiberQuestionWeight, ha, hb, and_self, ↓reduceIte, Game.repeat_questionWeight, + ha', hb', and_false, mul_zero, zero_mul, and_true] simpa only [Game.repeat_questionWeight] using (exactQuestionWeight_rectangle G n D seed history x y xs xs' ys ys' @@ -2597,7 +2596,7 @@ theorem arbitrarily_large_witness_of_not_hasExponentialBound rw [← Real.exp_add] congr 1 ring - linarith [hv n] + linarith only [hn, h_lower, hv n] refine ⟨n, hN, ?_⟩ have h_prefactor : 1 ≤ Real.exp (c * (N : ℝ)) := Real.one_le_exp (mul_nonneg hc.le (Nat.cast_nonneg _)) @@ -2691,7 +2690,7 @@ theorem expectation_le_add_totalVariation ring _ ≤ (∑ i, q i * f i) + ∑ i, U * max (p i - q i) 0 := by - linarith + linarith only [hsum] _ = (∑ i, q i * f i) + U * finiteTotalVariation p q := by rw [← Finset.mul_sum, hpositive] @@ -2709,7 +2708,7 @@ theorem winning_expectation_transfer q p win hq hp (1 : ℝ) hzero hone rw [← finiteTotalVariation_comm p q] at h norm_num at h ⊢ - linarith + linarith only [h] end @@ -2906,8 +2905,7 @@ theorem matched_payoff_discard_le simp only [Bool.not_eq_true] at hi simp only [hi, Bool.false_eq_true, ↓reduceIte, mul_one, mul_zero, tsub_le_iff_right, zero_add, ge_iff_le] - linarith [mul_nonneg (nonnegative i) - (sub_nonneg.mpr hone)] + linarith only [mul_nonneg (nonnegative i) (sub_nonneg.mpr hone)] end @@ -2964,7 +2962,7 @@ theorem source_equation_twenty_one _ = _ := by rw [Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.mul_sum] ring - _ ≤ 32 * η := by linarith + _ ≤ 32 * η := by linarith only [hgamma, hphi] theorem weighted_rpow_mean_le {ι : Type*} [Fintype ι] @@ -3197,7 +3195,7 @@ private theorem fullCoordinateInsertedHistory_weight simp_rw [hpair] simp only [fullCoordinateInsertedHistory, fullCoordinateAnswerExtension, ↓reduceDIte, univ_eq_attach] - ring + ac_rfl private theorem conditionedAliceEffect_insert_eq_coordinate (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) @@ -3376,7 +3374,7 @@ theorem exists_repeatedStrategy_of_lt_entangledValue have hzero : repeatedEntangledValue G n = 0 := by change sSup values = 0 rw [heq, Real.sSup_empty] - linarith + linarith only [hr, hvalue, hzero] have hs : r < sSup values := by exact hvalue obtain ⟨v, ⟨S, hS⟩, hv⟩ := exists_lt_of_lt_csSup hnonempty hs @@ -3429,19 +3427,19 @@ theorem greedy_terminal_of_log_cost (1 - η) ^ T < θ := by have hbase : 1 - η ≤ Real.exp (-η) := by have h := Real.add_one_le_exp (-η) - linarith + linarith only [h] have hpow : (1 - η) ^ T ≤ Real.exp (-η) ^ T := pow_le_pow_left₀ (sub_nonneg.mpr hη_one) hbase T have hlog : -η * (T : ℝ) < Real.log θ := by rw [one_div, Real.log_inv] at hcost - linarith + linarith only [hcost] calc (1 - η) ^ T ≤ Real.exp (-η) ^ T := hpow _ = Real.exp (-η * (T : ℝ)) := by rw [← Real.exp_nat_mul] congr 1 - ring + ac_rfl _ < θ := (Real.exp_lt_exp.mpr hlog).trans_eq (Real.exp_log hθ) @@ -3465,7 +3463,6 @@ theorem sourceRate_mul_lt_divisorStopping have hcast : (n : ℝ) < 2 * ((n / q : ℕ) : ℝ) * (q : ℝ) := by exact_mod_cast divisorStopping_nat_bound hq hqn - have hqreal : 0 < (q : ℝ) := by exact_mod_cast hq have hT : 0 < ((n / q : ℕ) : ℝ) := by exact_mod_cast ((Nat.le_div_iff_mul_le hq).2 (by simpa only [one_mul] using hqn) : 1 ≤ n / q) @@ -3481,7 +3478,7 @@ theorem sourceRate_mul_lt_divisorStopping _ < η * ((n / q : ℕ) : ℝ) := by have hpositive : 0 < η * ((n / q : ℕ) : ℝ) := mul_pos hη hT - linarith + linarith only [hpositive] theorem repeatedStrategy_exists_divisor_greedy_conditioning (G : Game X Y A B) (n : ℕ) @@ -3517,7 +3514,7 @@ theorem repeatedStrategy_exists_divisor_greedy_conditioning Real.log S.winProbability := (Real.lt_log_iff_exp_lt hθ).mpr hwitness rw [one_div, Real.log_inv] - linarith + linarith only [hlog'] have hterminal : (1 - η) ^ (n / q) < S.winProbability := by apply greedy_terminal_of_log_cost hθ hη_one @@ -3712,7 +3709,7 @@ theorem uniformRemainingFailure_lt_of_failure_sum rw [← Finset.sum_div] apply (div_lt_iff₀ hmreal).mpr apply (div_lt_iff₀ hp).mpr - linarith + linarith only [hfailure] end FiniteSamples @@ -3954,10 +3951,7 @@ theorem bornWeighted_normalized_distance (le_div_iff₀ hu_pos).mp hdist have hsquare := mul_self_le_mul_self (mul_nonneg (norm_nonneg _) (norm_nonneg u)) hscaled - linarith [sq_nonneg - (‖normalizeOrDefault fallback u - - normalizeOrDefault fallback v‖ * ‖u‖), - sq_nonneg (‖u - v‖)] + linarith only [hsquare] end ActualPurificationHistories @@ -4034,7 +4028,7 @@ private theorem fullCoordinateInsertedHistory_winIndicator_eq G.predicate (r.aliceConditioned j) (r.bobConditioned j) (α j) (β j) = true then (1 : ℝ) else 0) * (if G.predicate x y a b = true then (1 : ℝ) else 0) - split_ifs with hall hD hi <;> aesop + simp only [hiff, ite_and, ite_mul, one_mul, zero_mul] private def fullCoordinateInsertedHiddenAliceEquiv {X : Type*} {n : ℕ} @@ -4439,7 +4433,7 @@ private theorem fullCoordinateWeightedInsertedSum rw [fullCoordinateInsertedHistory_weight G D L i hiD r x y] rw [fullCoordinateInsertedHistory_winIndicator_eq G D L i hiD r x y α a β b] - ring + ac_rfl private def fullCoordinateAcceptedPostselectedMass (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) @@ -4635,7 +4629,7 @@ private theorem sourceHistoryAcceptedMass_eq_uniform rw [Finset.sum_mul] apply Finset.sum_congr rfl intro k _ - ring + ac_rfl theorem sourceHistoryAcceptedMass_eq_remaining_average (G : Game X Y A B) (n : ℕ) @@ -4722,7 +4716,7 @@ theorem sourceHistoryAcceptedMass_gt_of_greedy (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D i) < ((Finset.univ \ D).card : ℝ) * (η * p) at hgreedy - linarith [hgreedy, hfails] + linarith only [hfails, hgreedy] end @@ -4786,8 +4780,7 @@ theorem taggedTensorVector_norm simp only [hB, ↓reduceDIte, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, sum_const_zero] _ = _ := by simp only [↓reduceDIte] - nlinarith [norm_nonneg (taggedTensorVector r z), - norm_nonneg z] + exact (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp hsquare omit [Fintype R] [∀ r, Fintype (ι r)] in theorem taggedTensorVector_sub @@ -4799,7 +4792,7 @@ theorem taggedTensorVector_sub rcases q with ⟨a, b⟩ rcases a with a | ⟨rA, a⟩ <;> rcases b with b | ⟨rB, b⟩ <;> simp only [taggedTensorVector, PiLp.sub_apply, sub_zero] - split_ifs <;> simp + split_ifs <;> simp only [sub_self] end TaggedTensorBlocks @@ -4818,7 +4811,7 @@ theorem martingaleRate_nonneg G n S D π k) have hbudget := aliceMartingaleEntropyBudget G n S D hm hp - nlinarith + nlinarith only [hnonnegative, hbudget, hp] end @@ -5029,7 +5022,7 @@ theorem conditionedEventDistribution_relativeEntropy _ = Real.log (1 / law.eventMass event) := by rw [← Finset.sum_mul, conditionedEventDistribution_sum law event positive] - ring + ac_rfl theorem conditionedEventDistribution_projection_relativeEntropy_le {Ω κ : Type*} [Fintype Ω] [Fintype κ] @@ -5165,10 +5158,10 @@ theorem finiteRelativeEntropy_uniform_le_log_card rw [hratio] apply mul_le_mul_of_nonneg_left _ (nonnegative z) apply Real.log_le_log (mul_pos hp hcardpos) - nlinarith + nlinarith only [hpone] _ = Real.log (Fintype.card Z : ℝ) := by rw [← Finset.sum_mul, normalized] - ring + ac_rfl /-- The uniform flag reference construction used in the quantum parallel-repetition argument. -/ def uniformFlagReference @@ -5209,7 +5202,7 @@ theorem uniformFlagReference_firstMarginal change (∑ z : Z, prior ω * finiteUniformWeight Z) = prior ω rw [← Finset.mul_sum, finiteUniformWeight_sum positive] - ring + ac_rfl theorem uniformFlagReference_conditional {Ω Z : Type*} [Fintype Z] @@ -5313,7 +5306,7 @@ theorem uniformFlagRelativeEntropy_le · exact positive _ = Real.log (Fintype.card Z : ℝ) := by rw [← Finset.sum_mul, hmarginal_normalized] - ring + ac_rfl theorem finiteRelativeEntropy_nonneg {Ω : Type*} [Fintype Ω] @@ -5526,7 +5519,7 @@ theorem reversePartition_relativeEntropy_budget (2 * cost / (Fintype.card M : ℝ)) := by ring _ = 2 * cost / (Fintype.card M : ℝ) := by rw [← Finset.sum_mul, fairPartitionWeight_sum (α := M)] - ring + ac_rfl end @@ -5615,7 +5608,7 @@ theorem conditionedAnswerFlag_log_card postselectionLogCost G n S D = -Real.log (repeatedPostselectionMass G n S D) := by simp only [postselectionLogCost, one_div, Real.log_inv] - linarith + linarith only [hcost, hsplit, hpost] end @@ -6499,7 +6492,7 @@ private theorem exactFiber_born_of_rank_one (fun z : ℝ => z * bornTracePairing S.state.matrix (EA xs) (EB ys)) hrank field_simp [nonzero] - linarith [hborn] + linarith only [hborn] private theorem exactJointQuestionFilter_born (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) @@ -6885,8 +6878,8 @@ theorem exactFiberQuestionWeight_aliceMixed_rectangle D seed history y ys <;> by_cases hb' : exactBobQuestionCompatible D seed history y' ys' <;> - simp [exactFiberQuestionWeight, - ha, ha', hb, hb'] + simp only [exactFiberQuestionWeight, ha, hb, and_self, ↓reduceIte, Game.repeat_questionWeight, + ha', hb', and_false, mul_zero, zero_mul, and_true] simpa only [Game.repeat_questionWeight] using (exactQuestionWeight_aliceMixed_rectangle G n D seed history x y y' xs xs' ys ys' @@ -6992,8 +6985,8 @@ theorem exactFiberQuestionWeight_bobMixed_rectangle D seed history y ys <;> by_cases hb' : exactBobQuestionCompatible D seed history y ys' <;> - simp [exactFiberQuestionWeight, - ha, ha', hb, hb'] + simp only [exactFiberQuestionWeight, ha, hb, and_self, ↓reduceIte, Game.repeat_questionWeight, + ha', hb', and_false, mul_zero, zero_mul, and_true] simpa only [Game.repeat_questionWeight] using (exactQuestionWeight_bobMixed_rectangle G n D seed history x x' y xs xs' ys ys' @@ -7322,7 +7315,7 @@ private theorem exactAliceConditionalMatrix_eq_joint G n D seed history x) • E xs) := by apply Finset.sum_congr rfl intro ys _ - split_ifs <;> simp + split_ifs <;> simp only [zero_div, zero_smul] _ = ((∑ ys : Fin n → Y, if exactRevealCode D seed (xs, ys) = history ∧ xs seed.coordinate.val = x @@ -7405,7 +7398,7 @@ private theorem exactBobConditionalMatrix_eq_joint G n D seed history y) • E ys) := by apply Finset.sum_congr rfl intro xs _ - split_ifs <;> simp + split_ifs <;> simp only [zero_div, zero_smul] _ = ((∑ xs : Fin n → X, if exactRevealCode D seed (xs, ys) = history ∧ ys seed.coordinate.val = y diff --git a/LeanPool/QuantumParallelRepetition/Part05.lean b/LeanPool/QuantumParallelRepetition/Part05.lean index 4a4c1bb503..d17a21ad11 100644 --- a/LeanPool/QuantumParallelRepetition/Part05.lean +++ b/LeanPool/QuantumParallelRepetition/Part05.lean @@ -210,7 +210,7 @@ theorem exactFixedBobQuestionMass_insert simp only [Finset.mem_insert_self, ↓reduceIte, Function.update_self, fresh] rw [← G.marginalX_mul_conditionalYGivenX (xs j) y] - ring + ac_rfl theorem exactFixedAliceQuestionMass_insert (G : Game X Y A B) (n : ℕ) @@ -252,7 +252,7 @@ theorem exactFixedAliceQuestionMass_insert simp only [Finset.mem_insert_self, ↓reduceIte, Function.update_self, fresh] rw [← G.marginalY_mul_conditionalXGivenY x (ys j)] - ring + ac_rfl end @@ -431,7 +431,7 @@ private theorem exactReverseLeftSeedWeight_eq_forward Nat.cast_mul, Nat.cast_add, Nat.cast_one, Nat.cast_pow] field_simp - ring + ac_rfl private theorem exactReverseRightSeedWeight_eq_forward {M : Type*} [Fintype M] [DecidableEq M] @@ -448,7 +448,7 @@ private theorem exactReverseRightSeedWeight_eq_forward Nat.cast_mul, Nat.cast_add, Nat.cast_one, Nat.cast_pow] field_simp - ring + ac_rfl variable {X Y A B : Type*} variable [Fintype X] [Fintype Y] [Fintype A] [Fintype B] @@ -979,7 +979,7 @@ private theorem exactFairAliceHistoryVariation_le_entropy have hle := G.questionWeight_le_marginalY x y have hnonneg := G.weight_nonneg x y rw [hy] at hle - linarith + linarith only [hnonneg, hle] simp only [hzero, zero_mul, sum_const_zero, hy, Std.le_refl] · have hypos : 0 < G.marginalY y := lt_of_le_of_ne (G.marginalY_nonneg y) (Ne.symm hy) @@ -997,7 +997,7 @@ private theorem exactFairAliceHistoryVariation_le_entropy apply Finset.sum_congr rfl intro x _ rw [← G.marginalY_mul_conditionalXGivenY x y] - ring + ac_rfl _ ≤ _ := mul_le_mul_of_nonneg_left hlocal (G.marginalY_nonneg y) private theorem exactFairBobHistoryVariation_le_entropy @@ -1015,7 +1015,7 @@ private theorem exactFairBobHistoryVariation_le_entropy have hle := G.questionWeight_le_marginalX x y have hnonneg := G.weight_nonneg x y rw [hx] at hle - linarith + linarith only [hnonneg, hle] simp only [hzero, zero_mul, sum_const_zero, hx, Std.le_refl] · have hxpos : 0 < G.marginalX x := lt_of_le_of_ne (G.marginalX_nonneg x) (Ne.symm hx) @@ -1033,7 +1033,7 @@ private theorem exactFairBobHistoryVariation_le_entropy apply Finset.sum_congr rfl intro y _ rw [← G.marginalX_mul_conditionalYGivenX x y] - ring + ac_rfl _ ≤ _ := mul_le_mul_of_nonneg_left hlocal (G.marginalX_nonneg x) /-- The probability weight for exact fair history prior. -/ @@ -2067,8 +2067,9 @@ theorem exactReverseLeftSide_complement simp only [exactRight, ne_eq, mem_filter, mem_univ, not_true_eq_false, false_and, and_false, exactReverseLeftSide, mem_sdiff, mem_insert, true_or] · cases hbit : seed.partition j <;> - simp [exactRight, exactLeft, - exactReverseLeftSide, hcoordinate, hbit] + simp only [exactRight, ne_eq, mem_filter, mem_univ, hcoordinate, not_false_eq_true, hbit, + Bool.false_eq_true, and_false, exactReverseLeftSide, exactLeft, mem_sdiff, mem_insert, + and_self, or_true, not_true_eq_false, Bool.true_eq_false, or_self] theorem exactReverseRightSide_complement {M : Type*} [Fintype M] [DecidableEq M] @@ -2081,8 +2082,9 @@ theorem exactReverseRightSide_complement simp only [exactLeft, ne_eq, mem_filter, mem_univ, not_true_eq_false, false_and, and_false, exactReverseRightSide, mem_sdiff, mem_insert, true_or] · cases hbit : seed.partition j <;> - simp [exactRight, exactLeft, - exactReverseRightSide, hcoordinate, hbit] + simp only [exactLeft, ne_eq, mem_filter, mem_univ, hcoordinate, not_false_eq_true, hbit, + and_self, exactReverseRightSide, exactRight, mem_sdiff, mem_insert, Bool.false_eq_true, + and_false, or_self, Bool.true_eq_false, or_true, not_true_eq_false] /-- The data context recording exact reverse alice. -/ def exactReverseAliceContext @@ -2661,7 +2663,7 @@ theorem exactPrefixEntropyIncrement_eq_conditional finiteRelativeEntropy (jointConditional nextJoint context) (jointConditional nextPrior context) at hchain - linarith + linarith only [hnext_entropy, hchain] end @@ -2694,9 +2696,10 @@ theorem exactReverseAliceCanonicalPartition_side · subst j simp only [mem_insert, true_or, member] · by_cases hs : j ∈ side <;> - simp [exactLeft, - exactReverseAliceCanonicalPartition, - hj, hs] + simp only [exactLeft, ne_eq, exactReverseAliceCanonicalPartition, Bool.ite_true_right, + Bool.or_false, Bool.ite_eq_false_distrib, Bool.not_eq_eq_eq_not, Bool.not_false, + decide_eq_true_eq, mem_insert, hj, mem_filter, mem_univ, not_false_eq_true, ↓reduceIte, + hs, and_self, or_true, and_false, or_self] private theorem exactReverseAliceCanonicalPartition_unique {M : Type*} [Fintype M] [DecidableEq M] @@ -2761,9 +2764,9 @@ theorem exactReverseBobCanonicalPartition_side · subst j simp only [mem_insert, true_or, member] · by_cases hs : j ∈ side <;> - simp [exactRight, - exactReverseBobCanonicalPartition, - hj, hs] + simp only [exactRight, ne_eq, exactReverseBobCanonicalPartition, Bool.ite_false_right, + Bool.and_true, Bool.ite_eq_true_distrib, decide_eq_true_eq, mem_insert, hj, mem_filter, + mem_univ, not_false_eq_true, ↓reduceIte, hs, and_self, or_true, and_false, or_self] private theorem exactReverseBobCanonicalPartition_unique {M : Type*} [Fintype M] [DecidableEq M] @@ -2845,7 +2848,7 @@ theorem exactFiniteIndicator_sum rw [Finset.sum_mul] apply Finset.sum_congr rfl intro t _ - split_ifs <;> simp + split_ifs <;> simp only [one_mul, zero_mul] _ = (Fintype.card {t : T // predicate t} : ℝ) * weight := by simp only [sum_boole, Fintype.card_subtype] @@ -3166,7 +3169,7 @@ theorem exactReverseAliceConditionalSeedWeight_sum apply Finset.sum_congr rfl intro seed _ unfold exactReverseAliceConditionalSeedWeight - split_ifs <;> simp + split_ifs <;> simp only [zero_div] _ = groupedMass exactReverseLeftSide exactSeedWeight side / reversePartitionWeight side := by @@ -3196,7 +3199,7 @@ theorem exactReverseBobConditionalSeedWeight_sum apply Finset.sum_congr rfl intro seed _ unfold exactReverseBobConditionalSeedWeight - split_ifs <;> simp + split_ifs <;> simp only [zero_div] _ = groupedMass exactReverseRightSide exactSeedWeight side / reversePartitionWeight side := by @@ -3334,7 +3337,7 @@ theorem reweightedSeedWinEventMass rw [Finset.mul_sum] apply Finset.sum_congr rfl intro outcome _ - split_ifs <;> simp + split_ifs <;> simp only [mul_zero] simp_rw [hinner] rw [← Finset.sum_mul, seedLaw.weight_sum] simp only [sum_ite_mem, univ_inter, one_mul] @@ -4710,9 +4713,10 @@ theorem exactReverseAliceCanonicalPartition_otherSide simp only [exactRight, ne_eq, mem_filter, mem_univ, not_true_eq_false, false_and, and_false, mem_sdiff, member] · by_cases belongs : j ∈ side <;> - simp [exactRight, - exactReverseAliceCanonicalPartition, - marked, belongs] + simp only [exactRight, ne_eq, exactReverseAliceCanonicalPartition, Bool.ite_true_right, + Bool.or_false, Bool.ite_eq_true_distrib, Bool.not_eq_eq_eq_not, Bool.not_true, + decide_eq_false_iff_not, mem_filter, mem_univ, marked, not_false_eq_true, ↓reduceIte, + belongs, not_true_eq_false, and_false, mem_sdiff, and_self] theorem exactReverseBobCanonicalPartition_otherSide {M : Type*} [Fintype M] [DecidableEq M] @@ -4728,9 +4732,10 @@ theorem exactReverseBobCanonicalPartition_otherSide simp only [exactLeft, ne_eq, mem_filter, mem_univ, not_true_eq_false, false_and, and_false, mem_sdiff, member] · by_cases belongs : j ∈ side <;> - simp [exactLeft, - exactReverseBobCanonicalPartition, - marked, belongs] + simp only [exactLeft, ne_eq, exactReverseBobCanonicalPartition, Bool.ite_false_right, + Bool.and_true, Bool.ite_eq_false_distrib, decide_eq_false_iff_not, mem_filter, mem_univ, + marked, not_false_eq_true, ↓reduceIte, belongs, not_true_eq_false, and_false, mem_sdiff, + and_self] theorem exactReverseAliceCanonicalPartition_card {M : Type*} [Fintype M] [DecidableEq M] @@ -6332,16 +6337,14 @@ theorem exactRevealCode_splitAt_independent have different : j.val ≠ seed.coordinate.val := by intro h exact hiD (h ▸ j.property) - simp only [ne_eq, Equiv.funSplitAt, Equiv.piSplitAt, eq_rec_constant, Equiv.symm_mk, - Equiv.coe_fn_mk, different, ↓reduceDIte] + simp only [ne_eq, Equiv.funSplitAt_symm_apply, different, ↓reduceDIte] · funext j have hiD : seed.coordinate.val ∉ D := (Finset.mem_sdiff.mp seed.coordinate.property).2 have different : j.val ≠ seed.coordinate.val := by intro h exact hiD (h ▸ j.property) - simp only [ne_eq, Equiv.funSplitAt, Equiv.piSplitAt, eq_rec_constant, Equiv.symm_mk, - Equiv.coe_fn_mk, different, ↓reduceDIte] + simp only [ne_eq, Equiv.funSplitAt_symm_apply, different, ↓reduceDIte] · funext j have different : j.val.val ≠ seed.coordinate.val := by intro h @@ -6351,8 +6354,7 @@ theorem exactRevealCode_splitAt_independent simpa only [same] using j.property exact exactLeft_coordinate_not_mem seed.coordinate seed.partition mem - simp only [ne_eq, Equiv.funSplitAt, Equiv.piSplitAt, eq_rec_constant, Equiv.symm_mk, - Equiv.coe_fn_mk, different, ↓reduceDIte] + simp only [ne_eq, Equiv.funSplitAt_symm_apply, different, ↓reduceDIte] · funext j have different : j.val.val ≠ seed.coordinate.val := by intro h @@ -6362,8 +6364,7 @@ theorem exactRevealCode_splitAt_independent simpa only [same] using j.property exact exactRight_coordinate_not_mem seed.coordinate seed.partition mem - simp only [ne_eq, Equiv.funSplitAt, Equiv.piSplitAt, eq_rec_constant, Equiv.symm_mk, - Equiv.coe_fn_mk, different, ↓reduceDIte] + simp only [ne_eq, Equiv.funSplitAt_symm_apply, different, ↓reduceDIte] · funext j have different : j.val.val ≠ seed.coordinate.val := by intro h @@ -6371,8 +6372,7 @@ theorem exactRevealCode_splitAt_independent have hleft := exactLeftPrefix_subset seed j.property exact exactLeft_coordinate_not_mem seed.coordinate seed.partition (same ▸ hleft) - simp only [ne_eq, Equiv.funSplitAt, Equiv.piSplitAt, eq_rec_constant, Equiv.symm_mk, - Equiv.coe_fn_mk, different, ↓reduceDIte] + simp only [ne_eq, Equiv.funSplitAt_symm_apply, different, ↓reduceDIte] · funext j have different : j.val.val ≠ seed.coordinate.val := by intro h @@ -6380,8 +6380,7 @@ theorem exactRevealCode_splitAt_independent have hright := exactRightPrefix_subset seed j.property exact exactRight_coordinate_not_mem seed.coordinate seed.partition (same ▸ hright) - simp only [ne_eq, Equiv.funSplitAt, Equiv.piSplitAt, eq_rec_constant, Equiv.symm_mk, - Equiv.coe_fn_mk, different, ↓reduceDIte] + simp only [ne_eq, Equiv.funSplitAt_symm_apply, different, ↓reduceDIte] theorem exactRepeatedQuestionWeight_splitAt_joint (G : Game X Y A B) (n : ℕ) (i : Fin n) @@ -6720,7 +6719,7 @@ theorem exactJointQuestionMass_eq_reveal_mul_question simp only [one_mul] rw [exactJointQuestionMass_eq_question_mul_tail, ← htail] - ring + ac_rfl end @@ -7091,7 +7090,7 @@ theorem exactLocallySampleableLaw_eq_fair_born · simp only [code, ↓reduceIte, mul_zero, zero_div] _ = _ := by rw [exactFairFullOutcomeBornMass_eq_reveal_question_norm] - ring + ac_rfl convert hcalc using 1 apply Finset.sum_congr rfl intro o _ @@ -7334,7 +7333,7 @@ private theorem exactFairPsiPhiDistance_mul_postselection_le have hscaled := mul_le_mul_of_nonneg_left hnorm hw unfold exactFairHistoryPriorWeight at hscaled ⊢ field_simp [positive.ne'] - linarith + linarith only [hscaled] · rw [ite_eq_right accepted, exactLocallySampleableLaw_eq_fair_born, ite_eq_right accepted] @@ -7351,7 +7350,7 @@ private theorem exactFairPsiPhiDistance_mul_postselection_le intro y _ apply Finset.sum_congr rfl intro x _ - ring + ac_rfl · simp only [accepted, ↓reduceIte, sum_const_zero, mul_zero] private theorem exactFairGammaPsiDistance_mul_postselection_le @@ -7415,7 +7414,7 @@ private theorem exactFairGammaPsiDistance_mul_postselection_le have hscaled := mul_le_mul_of_nonneg_left hnorm hw unfold exactFairHistoryPriorWeight at hscaled ⊢ field_simp [positive.ne'] - linarith + linarith only [hscaled] · rw [ite_eq_right accepted, exactLocallySampleableLaw_eq_fair_born, ite_eq_right accepted] @@ -7434,7 +7433,7 @@ private theorem exactFairGammaPsiDistance_mul_postselection_le apply Finset.sum_congr rfl intro y _ rw [norm_sub_rev] - ring + ac_rfl · simp only [accepted, ↓reduceIte, sum_const_zero, mul_zero] /-- The numerical bound for exact fair operator entropy. -/ @@ -7468,7 +7467,7 @@ theorem exactSourceStateDistanceBound_of_fair_operator_entropy exactLocallySampleableLaw G n S D t * ‖exactSourceTupleGamma G n S D t - exactSourceTuplePsi G n S D t‖ ^ 2) ≤ 8 * η - nlinarith + nlinarith only [hv, hj, hb, positive] · have hv := exactFairPsiPhiDistance_mul_postselection_le G n S D positive have hj := exactAcceptedFairAliceVariation_le_entropy @@ -7483,7 +7482,7 @@ theorem exactSourceStateDistanceBound_of_fair_operator_entropy exactLocallySampleableLaw G n S D t * ‖exactSourceTuplePsi G n S D t - exactSourceTuplePhi G n S D t‖ ^ 2) ≤ 8 * η - nlinarith + nlinarith only [hv, hj, ha, positive] end diff --git a/LeanPool/QuantumParallelRepetition/Part06.lean b/LeanPool/QuantumParallelRepetition/Part06.lean index 4d14f94cc5..dcfeb0faa2 100644 --- a/LeanPool/QuantumParallelRepetition/Part06.lean +++ b/LeanPool/QuantumParallelRepetition/Part06.lean @@ -60,7 +60,7 @@ theorem exactAliceQuestionConditionalWeight_sum rw [Finset.sum_div] apply Finset.sum_congr rfl intro q _ - split <;> simp + split <;> simp only [zero_div] _ = exactAliceQuestionMass G n D seed history x / exactAliceQuestionMass G n D seed history x := by rfl @@ -100,7 +100,7 @@ theorem exactBobQuestionConditionalWeight_sum rw [Finset.sum_div] apply Finset.sum_congr rfl intro q _ - split <;> simp + split <;> simp only [zero_div] _ = exactBobQuestionMass G n D seed history y / exactBobQuestionMass G n D seed history y := by rfl @@ -155,7 +155,7 @@ theorem exactAliceQuestionFilter_complement_posSemidef apply Finset.sum_congr rfl intro q _ dsimp [w, E] - split <;> simp + split <;> simp only [zero_smul] have split : 1 - (∑ q, w q • E q) = (1 - (∑ q, w q)) • @@ -218,7 +218,7 @@ theorem exactBobQuestionFilter_complement_posSemidef apply Finset.sum_congr rfl intro q _ dsimp [w, E] - split <;> simp + split <;> simp only [zero_smul] have split : 1 - (∑ q, w q • E q) = (1 - (∑ q, w q)) • @@ -474,7 +474,7 @@ theorem exactFairAliceHistoryLowOperatorPotential_neg_le_entropy have bound := mul_le_mul_of_nonneg_left (exactFairAliceMean_spectral_entropy_le G n S D r y) (G.marginalY_nonneg y) - linarith + linarith only [bound] theorem exactFairBobHistoryLowOperatorPotential_neg_le_entropy (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) @@ -496,7 +496,7 @@ theorem exactFairBobHistoryLowOperatorPotential_neg_le_entropy have bound := mul_le_mul_of_nonneg_left (exactFairBobMean_spectral_entropy_le G n S D r x) (G.marginalX_nonneg x) - linarith + linarith only [bound] theorem exactReverseAliceFilterHighOperatorPotential_nonpos (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) @@ -1419,7 +1419,7 @@ private theorem exactAliceQuestionFilter_eq_jointPrefixOperatorFilter unfold exactPriorQuestionWeight rw [div_eq_mul_inv] congr 1 - ring + ac_rfl · rw [ite_eq_right (fun h => compatible (same.mp h)), ite_eq_right compatible, smul_zero] @@ -1491,7 +1491,7 @@ private theorem exactBobQuestionFilter_eq_jointPrefixOperatorFilter unfold exactPriorQuestionWeight rw [div_eq_mul_inv] congr 1 - ring + ac_rfl · rw [ite_eq_right (fun h => compatible (same.mp h)), ite_eq_right compatible, smul_zero] @@ -1860,7 +1860,7 @@ theorem exactFairAliceHistoryHighOperatorPotential_eq_joint intro y _ apply Finset.sum_congr rfl intro x _ - ring + ac_rfl _ = ∑ y : Y, ∑ x : X, G.questionWeight x y * bornTracePairing S.state.matrix (cfc (fun z : ℝ => z * Real.log z) @@ -1896,7 +1896,7 @@ theorem exactFairBobHistoryHighOperatorPotential_eq_joint apply Finset.sum_congr rfl intro y _ rw [← G.marginalX_mul_conditionalYGivenX x y] - ring + ac_rfl theorem exactFairAliceHistoryLowOperatorPotential_eq_joint (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) @@ -2024,7 +2024,7 @@ theorem exactFairAcceptedJointStatistic_reindex intro x _ apply Finset.sum_congr rfl intro y _ - ring + ac_rfl · simp only [accepted, ↓reduceIte, sum_const_zero] _ = ∑ history : ExactRevealHistory X Y D seed, ∑ x : X, ∑ y : Y, @@ -4041,7 +4041,7 @@ private theorem exactReverseAliceLowOperatorPotential_neg_le_scalarEntropy (exactRevealMass_nonneg G n D (exactReverseBobMarkerDecode side context marker) history) - linarith + linarith only [weighted] · simp only [accepted, ↓reduceIte, neg_zero, Std.le_refl] private theorem exactReverseAliceAlignedCfcPrefixPotential_last_nonpos @@ -4086,7 +4086,7 @@ private theorem exactReverseAliceFilterOperatorMarkerEntropy_sum_le_scalarEntrop rw [exactReverseAliceLowOperatorPotential_eq_question, exactReverseAliceLowQuestionPotential_eq_alignedPrefix] at low dsimp only at low - linarith + linarith only [nonempty, last, low] end @@ -4216,7 +4216,7 @@ private theorem exactReverseBobFilterOperatorMarkerEntropy_sum_le_scalarEntropy G n S D side context 0 ≤ exactReverseBobAcceptedScalarEntropy G n S D side context initial - linarith + linarith only [terminal, scalar] end @@ -4323,7 +4323,7 @@ theorem exactFairAliceMeanBornMass_eq_fullOutcome_sum Finset.mul_sum, Finset.mul_sum] apply Finset.sum_congr rfl intro x _ - ring + ac_rfl _ = ∑ x : X, ∑ y : Y, exactRevealMass G n D r.seed r.history * G.questionWeight x y * @@ -4383,7 +4383,7 @@ theorem exactFairBobMeanBornMass_eq_fullOutcome_sum Finset.mul_sum, Finset.mul_sum] apply Finset.sum_congr rfl intro y _ - ring + ac_rfl _ = ∑ x : X, ∑ y : Y, exactRevealMass G n D r.seed r.history * G.questionWeight x y * @@ -4653,7 +4653,7 @@ private theorem exactFairAliceScalarCountingWeight_sum_le nsmul_eq_mul, Nat.cast_pow, mul_sum, fullHistoryAnswerCount, mul_assoc, mul_comm] _ = _ := by rw [exactRevealMass_sum, G.marginalY_normalized] - ring + ac_rfl private theorem exactFairBobScalarCountingWeight_sum_le (G : Game X Y A B) (n : ℕ) @@ -4698,7 +4698,7 @@ private theorem exactFairBobScalarCountingWeight_sum_le nsmul_eq_mul, Nat.cast_pow, mul_sum, fullHistoryAnswerCount, mul_assoc, mul_comm] _ = _ := by rw [exactRevealMass_sum, G.marginalX_normalized] - ring + ac_rfl private theorem exactFairAliceScalarBornMass_sum (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) @@ -4740,7 +4740,7 @@ private theorem exactFairAliceScalarBornMass_sum ite_eq_left accepted, Finset.mul_sum] apply Finset.sum_congr rfl intro y _ - ring + ac_rfl · simp only [exactFairAliceScalarCountingWeight, accepted, ↓reduceIte, zero_mul, sum_const_zero] _ = _ := exactFairAliceMeanAcceptedBornMass_sum @@ -4786,7 +4786,7 @@ private theorem exactFairBobScalarBornMass_sum ite_eq_left accepted, Finset.mul_sum] apply Finset.sum_congr rfl intro x _ - ring + ac_rfl · simp only [exactFairBobScalarCountingWeight, accepted, ↓reduceIte, zero_mul, sum_const_zero] _ = _ := exactFairBobMeanAcceptedBornMass_sum @@ -4892,7 +4892,7 @@ private theorem exactFairAliceSeedScalarEntropy_eq_weighted Finset.mul_sum] apply Finset.sum_congr rfl intro y _ - ring + ac_rfl · simp only [accepted, ↓reduceIte, exactFairAliceScalarCountingWeight, zero_mul, sum_const_zero] private theorem exactFairBobSeedScalarEntropy_eq_weighted @@ -4921,7 +4921,7 @@ private theorem exactFairBobSeedScalarEntropy_eq_weighted Finset.mul_sum] apply Finset.sum_congr rfl intro x _ - ring + ac_rfl · simp only [accepted, ↓reduceIte, exactFairBobScalarCountingWeight, zero_mul, sum_const_zero] private theorem exactFairAliceSeedScalarEntropy_le @@ -5093,7 +5093,7 @@ theorem fullHistoryAnswerCount_pos_of_postselection (fullHistoryAtomCountingWeight_nonneg G D L t) (fullHistoryAtomBornMass_le_one G n S D L t) have hsecond := fullHistoryAtomCountingWeight_sum_le G D L - linarith + linarith only [hp, hmass, hfirst, hsecond] theorem divisor_greedy_remaining_bounds {n q : ℕ} (hq : 2 ≤ q) @@ -5164,7 +5164,7 @@ private theorem divisor_greedy_log_cost_per_remaining_le (η / (4 * (q : ℝ))) * (n : ℝ) := by have hlog := (Real.lt_log_iff_exp_lt hθ).mpr hwitness rw [one_div, Real.log_inv] - linarith + linarith only [hlog] have hlogp : Real.log (1 / p) ≤ (η / (4 * (q : ℝ))) * (n : ℝ) := by @@ -5176,7 +5176,7 @@ private theorem divisor_greedy_log_cost_per_remaining_le (η / (4 * (q : ℝ))) * (n : ℝ) := by rw [Real.log_div hN.ne' hp.ne'] rw [one_div, Real.log_inv] at hlogp - linarith + linarith only [hcount, hlogp] obtain ⟨hmnat, hnmnat, hdqmnat⟩ := divisor_greedy_remaining_bounds hq hD have hm : 0 < (m : ℝ) := by @@ -5243,7 +5243,7 @@ private theorem exists_source_rounding_divisor have hsmall : C / (q : ℝ) < δ ^ 2 := by apply (div_lt_iff₀ hqreal).mpr have hcross := (div_lt_iff₀ hsquare).mp hthreshold - linarith [hC] + linarith only [hcross] refine ⟨q, hqnat, ?_⟩ calc 8 * K * @@ -5295,7 +5295,6 @@ theorem arbitrarily_large_purified_divisor_greedy_conditioning_with_rounding refine ⟨q, hq, ?_⟩ intro N₀ have hqpos : 0 < q := by omega - have hqreal : 0 < (q : ℝ) := by exact_mod_cast hqpos have hrate : 0 < η / (4 * (q : ℝ)) := by positivity obtain ⟨n, hn, S, hS⟩ := arbitrarily_large_purifiedRepeatedStrategy_of_subexponentialWitness @@ -5409,7 +5408,7 @@ theorem exactSourceClassicalInformationRate_le_three_martingaleRate lt_of_le_of_ne denominator_nonnegative (Ne.symm denominator_zero) apply (div_le_iff₀ denominator_positive).2 field_simp - linarith + linarith only [answer_nonnegative] theorem exactSourcePinskerRate_le_half_of_martingaleRate (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) @@ -5426,7 +5425,7 @@ theorem exactSourcePinskerRate_le_half_of_martingaleRate · have information := exactSourceClassicalInformationRate_le_three_martingaleRate G n S D positive - nlinarith + nlinarith only [rate_bound, information] theorem exact_arbitrarily_large_conditioning_of_subexponentialWitness (G : Game X Y A B) @@ -5492,7 +5491,7 @@ theorem exact_arbitrarily_large_conditioning_of_subexponentialWitness martingaleRate G n actual D ≤ rateTolerance ^ 2 / 8 := by apply (le_div_iff₀ (by norm_num : (0 : ℝ) < 8)).2 - linarith + linarith only [scaled_rate] exact ⟨n, beyond, actual, D, actual_positive, postselection_positive, remaining_positive, failure_small, actual_rate, @@ -5551,7 +5550,7 @@ theorem exactReversePartitionInverseCard_le intro side _ unfold forwardMarkedPartitionWeight ring - _ = _ := by rw [fairPartitionWeight_sum]; ring + _ = _ := by rw [fairPartitionWeight_sum]; ac_rfl theorem exactReverseBobSeedInverseCard_le {M : Type*} [Fintype M] [DecidableEq M] : @@ -5850,7 +5849,7 @@ theorem unconditionalLiterature_sqrt_two_mul_sqrt_thirtytwo 8 * Real.sqrt 2 * Real.sqrt (32 * η) = 8 * Real.sqrt ((2 : ℝ) * (32 * η)) := by rw [Real.sqrt_mul (by norm_num : (0 : ℝ) ≤ 2)] - ring + ac_rfl _ = 8 * Real.sqrt ((64 : ℝ) * η) := by congr 2 ring @@ -5900,7 +5899,7 @@ theorem unconditionalLiterature_weightedAsynchronous_le apply Finset.sum_congr rfl intro i _ ring - _ = _ := by rw [weight_normalized]; ring + _ = _ := by rw [weight_normalized]; ac_rfl _ ≤ 8 * Real.sqrt 2 * Real.sqrt (32 * η) + δ := by gcongr _ = 64 * Real.sqrt η + δ := by @@ -6484,7 +6483,8 @@ private theorem dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyConditionMask] cases h : dSVDensityRationalCompleteStoppedOptionalLocalSchedule L flag i with - | none => simp [dSVDensityRationalCompleteStoppedOptionalLocalEffect] + | none => simp only [UnitaryGroup.inv_val, mul_one, SetLike.coe_mem, + Unitary.star_mul_self_of_mem, dSVDensityRationalCompleteStoppedOptionalLocalEffect] | some outcome => simpa only [UnitaryGroup.inv_val, dSVDensityRationalCompleteStoppedOptionalLocalEffect] using @@ -6800,7 +6800,7 @@ theorem dSVDensityRationalPublicLogPhasePhysicalAlignedLocalAction_apply intro x _ apply Finset.sum_congr rfl intro y _ - ring + ac_rfl · rfl /-- diff --git a/LeanPool/QuantumParallelRepetition/Part07.lean b/LeanPool/QuantumParallelRepetition/Part07.lean index c1165e62c2..1516f56ef5 100644 --- a/LeanPool/QuantumParallelRepetition/Part07.lean +++ b/LeanPool/QuantumParallelRepetition/Part07.lean @@ -236,7 +236,7 @@ private theorem dSVDensityRationalPureFlagBorn_partition_zero_succ alice bob z rw [dSVDensityRationalPureMatchedFlagBorn_zero_succ alice bob z] at actual - linarith + linarith only [actual] private theorem dSVDensityRationalPureFlagBorn_normalized_partition_zero_succ {A C : Type*} [Fintype A] [Fintype C] @@ -566,7 +566,7 @@ theorem have stages := dSVDensityRationalHeterogeneousPhysicalStopped_mass_partition grid dimension width schedule ξ ζ - linarith + linarith only [physical, stages] end @@ -613,7 +613,7 @@ theorem embezzlementState n ((finProdFinEquiv.symm q.1).2, (finProdFinEquiv.symm q.2).2)) - ring + ac_rfl theorem dSVDensityRationalMixedCanonicalPrefixPhysicalRawHarmonicTensor_eq @@ -1089,7 +1089,7 @@ theorem dSVDensityRationalPublicShiftedBucketMismatch_sum_le (((x + phase.val) / B : ℕ) : ℝ) + 1 ≤ (((y + phase.val) / B : ℕ) : ℝ) := by exact_mod_cast Nat.succ_le_of_lt strictly - linarith + linarith only [cast_bound] _ = (y : ℝ) - (x : ℝ) := by rw [Finset.sum_sub_distrib, dSVDensityRationalPublicShiftedQuotient_real_sum @@ -1209,11 +1209,11 @@ theorem dSVDensityRationalPublicLogRankFineLabel_abs_sub_le · have lower := neg_le_abs ((Q : ℝ) * Real.log ((max 1 r.val : ℕ) : ℝ) - (Q : ℝ) * Real.log ((max 1 s.val : ℕ) : ℝ)) - linarith [first.2, second.1] + linarith only [first, second, lower] · have upper := le_abs_self ((Q : ℝ) * Real.log ((max 1 r.val : ℕ) : ℝ) - (Q : ℝ) * Real.log ((max 1 s.val : ℕ) : ℝ)) - linarith [first.1, second.2] + linarith only [first, second, upper] private theorem dSVDensityRationalPublicLogRankPhaseWeightedCrossing_min_le @@ -1270,7 +1270,7 @@ private theorem min (r.val : ℝ) (s.val : ℝ) / (B : ℝ) := by have scaled := mul_le_mul_of_nonneg_left logarithmic (div_nonneg (Nat.cast_nonneg Q) positive_real.le) - linarith + linarith only [scaled] end @@ -1389,7 +1389,7 @@ theorem (representative.val : ℝ) < Real.exp (((B : ℝ) + 1) / (Q : ℝ)) - 1 rw [sub_div, div_self positive_representative.ne'] - linarith + linarith only [ratio] theorem dSVDensityRationalPublicLogRankBucketRepresentative_relative_abs_lt @@ -1455,7 +1455,8 @@ private theorem dSVDensityRationalPublicLogRankPhaseWeightedCrossing_le_one apply Finset.sum_le_sum intro phase _ split_ifs <;> - simp [dSVDensityRationalPublicLogRankPhaseWeight] + simp only [dSVDensityRationalPublicLogRankPhaseWeight, one_div, mul_zero, inv_nonneg, + Nat.cast_nonneg, mul_one, Std.le_refl] _ = 1 := dSVDensityRationalPublicLogRankPhaseWeight_sum positive @@ -1474,9 +1475,6 @@ private theorem Q B r s let m : ℝ := min (r.val : ℝ) (s.val : ℝ) let t : ℝ := |(r.val : ℝ) - (s.val : ℝ)| - have nonnegative : 0 ≤ x := - dSVDensityRationalPublicLogRankPhaseWeightedCrossing_nonneg - Q B r s have probability : x ≤ 1 := dSVDensityRationalPublicLogRankPhaseWeightedCrossing_le_one positive Q r s @@ -1501,7 +1499,7 @@ private theorem at main change (r.val : ℝ) * x ≤ ((Q : ℝ) / (B : ℝ) + 1) * t + m / (B : ℝ) - linarith + linarith only [extra, main] private theorem exists_proofDSVDensityRationalPublicBucketPhysicalQuantitativeMixedPrefixCleanup_sq @@ -1614,7 +1612,7 @@ private theorem (if bucket phase r = bucket phase s then (0 : ℝ) else 1) := by dsimp [base] - linarith + linarith only [variation] have averaged : (∑ phase : Fin B, dSVDensityRationalPublicLogRankPhaseWeight B phase * @@ -1683,7 +1681,7 @@ private theorem at crossing dsimp [bucket] at averaged dsimp [base] at averaged - linarith + linarith only [averaged, crossing] private def dSVDensityRationalHeterogeneousCommonStopSpectralAtomWeight {d : ℕ} (N : ℕ) @@ -1826,7 +1824,7 @@ private theorem finitePhaseWeightedDoubleSum_exchange rw [Finset.mul_sum] apply Finset.sum_congr rfl intro phase _ - ring + ac_rfl private theorem finiteDoubleSum_mul_add {I J : Type*} [Fintype I] [Fintype J] @@ -1841,12 +1839,12 @@ private theorem finiteDoubleSum_mul_add intro i _ apply Finset.sum_congr rfl intro j _ - ring + ac_rfl · apply Finset.sum_congr rfl intro i _ apply Finset.sum_congr rfl intro j _ - ring + ac_rfl theorem exists_proofDSVDensityRationalHeterogeneousCommonStopSpectralGaugeContinuity_sq @@ -1968,7 +1966,7 @@ theorem 16 * (Real.exp (((B : ℝ) + 1) / (Q : ℝ)) - 1)) * alice i + 8 * (alice i / (B : ℝ)) := by - linarith [min_bound] + linarith only [min_bound] _ = Kgap * gap i j + Kmass * alice i := by dsimp [Kmass] ring @@ -2150,7 +2148,7 @@ private theorem 0 ≤ Real.exp (((B : ℝ) + 1) / (Q : ℝ)) - 1 := by have exponential := Real.add_one_le_exp (((B : ℝ) + 1) / (Q : ℝ)) - linarith + linarith only [exponent_nonnegative, exponential] have Kmass_nonnegative : 0 ≤ Kmass := by dsimp [Kmass] positivity @@ -2226,8 +2224,7 @@ private theorem _ ≤ Kgap * dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule ξ ζ + Kmass := by - linarith [mul_nonneg Kmass_nonnegative - (sub_nonneg.mpr diagonal_budget)] + linarith only [grid, dimension, mul_nonneg Kmass_nonnegative (sub_nonneg.mpr diagonal_budget)] /-- The joint failure vector at a stage preceding the stopping position. -/ def dSVDensityRationalHeterogeneousStoppedCommonPrefixFailureCopy @@ -2402,7 +2399,7 @@ theorem unconditionalPublicBucket_exp_sub_one_le (show (1 - u) + u = (1 : ℝ) by ring) simp only [smul_eq_mul, mul_zero, zero_add, mul_one, Real.exp_zero] at chord - linarith + linarith only [chord] private def unconditionalPublicBucketLoss (B Q : ℕ) (asynchronous precision : ℝ) : ℝ := @@ -2439,7 +2436,7 @@ private theorem exists_proofUnconditionalPublicBucketBalance (div_le_iff₀ positive).mp lower have inverse_bound : 1 / (B : ℝ) ≤ t / 2 := by apply (div_le_iff₀ B_real_positive).mpr - linarith + linarith only [product_lower] have ceiling_upper : (B : ℝ) < 2 / t + 1 := by exact Nat.ceil_lt_add_one (by positivity : (0 : ℝ) ≤ 2 / t) have product_upper : (B : ℝ) * t < 2 + t := by @@ -2449,7 +2446,7 @@ private theorem exists_proofUnconditionalPublicBucketBalance _ = 2 + t := by field_simp have B_upper : (B : ℝ) ≤ 3 / t := by apply (le_div_iff₀ positive).mpr - linarith + linarith only [bounded, product_upper] have ratio_eq : (Q : ℝ) / (B : ℝ) = (B : ℝ) := by dsimp [Q] push_cast @@ -2465,7 +2462,7 @@ private theorem exists_proofUnconditionalPublicBucketBalance have Q_real : (Q : ℝ) = (B : ℝ) ^ 2 := by simp only [Nat.cast_pow, Q] rw [Q_real] - linarith + linarith only [B_at_least_one, multiply] have width_nonnegative : 0 ≤ ((B : ℝ) + 1) / (Q : ℝ) := by positivity have exponential_bound : @@ -2478,7 +2475,7 @@ private theorem exists_proofUnconditionalPublicBucketBalance width_nonnegative (width_bound.trans bounded) _ ≤ (Real.exp 1 - 1) * t := by have coefficient : 0 ≤ Real.exp 1 - 1 := by - linarith [Real.add_one_le_exp (1 : ℝ)] + linarith only [Real.add_one_le_exp (1 : ℝ)] exact mul_le_mul_of_nonneg_left width_bound coefficient refine ⟨B, Q, B_positive, Q_positive, inverse_bound, ratio_bound, width_bound, exponential_bound, ?_⟩ @@ -2505,7 +2502,7 @@ private theorem exists_proofUnconditionalPublicBucketBalance (by norm_num : (0 : ℝ) ≤ 10) have ten_piece : (10 : ℝ) ≤ 10 / t := by calc - (10 : ℝ) = 10 * 1 := by ring + (10 : ℝ) = 10 * 1 := by ac_rfl _ ≤ 10 * (1 / t) := ten_scaled _ = 10 / t := by ring have ratio_piece : @@ -2517,11 +2514,8 @@ private theorem exists_proofUnconditionalPublicBucketBalance 10 + 8 * ((Q : ℝ) / (B : ℝ)) ≤ 10 / t + 24 / t := add_le_add ten_piece ratio_piece _ = 34 / t := by ring - have exponential_scaled := - mul_le_mul_of_nonneg_left exponential_bound - (by norm_num : (0 : ℝ) ≤ 16) unfold unconditionalPublicBucketLoss - linarith + linarith only [exponential_bound, reciprocal, ratio_cost] theorem exists_proofUnconditionalStoppedCommonPrefixBalancedHazard {d N : ℕ} (grid : 0 < N) (dimension : 0 < d) @@ -2686,7 +2680,7 @@ theorem unconditionalPrefactor_balancedHazard_sqrt_le Real.sqrt a := by rw [coefficient_square, fourth_square] have quotient : (34 / Real.sqrt a) * a = 34 * Real.sqrt a := by field_simp [ne_of_gt root_positive] - linarith [root_square] + linarith only [root_square] apply Real.sqrt_le_iff.mpr constructor · positivity @@ -2699,7 +2693,7 @@ theorem unconditionalPrefactor_balancedHazard_sqrt_le (mul_nonneg (Real.sqrt_nonneg _) (Real.rpow_nonneg positive.le _)) rho_nonnegative - linarith [product_square] + linarith only [product_square, cross_nonnegative] theorem unconditionalPrefactor_smallHazard_twelfthRoot_le {eta alpha : ℝ} @@ -2724,13 +2718,11 @@ theorem unconditionalPrefactor_smallHazard_twelfthRoot_le have a_positive : 0 < a := by dsimp [a] have := Real.sqrt_nonneg eta - linarith + linarith only [alpha_third_positive, this] have eta_root_square : (Real.sqrt eta) ^ 2 = eta := Real.sq_sqrt eta_nonnegative have eta_bounded : eta ≤ 1 := by - have eta_root_bounded : Real.sqrt eta ≤ 1 := by - linarith [Real.sqrt_nonneg eta, alpha_third_positive] - nlinarith [Real.sqrt_nonneg eta] + nlinarith only [small, alpha_third_positive, eta_root_square, Real.sqrt_nonneg eta] have rho_nonnegative : 0 ≤ rho := by dsimp [rho] exact Real.rpow_nonneg alpha_positive.le _ @@ -2755,11 +2747,9 @@ theorem unconditionalPrefactor_smallHazard_twelfthRoot_le (eta ^ (1 / 12 : ℝ) + rho) change a ^ (1 / 4 : ℝ) ≤ 4 * eta ^ (1 / 12 : ℝ) + rho at quarter - linarith [mul_nonneg coefficient_root_nonnegative - (sub_nonneg.mpr quarter), - mul_nonneg coefficient_root_nonnegative rho_nonnegative, - mul_nonneg (show 0 ≤ (2 : ℝ) by norm_num) - eta_twelfth_nonnegative] + linarith only [eta_twelfth_nonnegative, balanced, + mul_nonneg coefficient_root_nonnegative (sub_nonneg.mpr quarter), + mul_nonneg coefficient_root_nonnegative rho_nonnegative] theorem unconditionalPrefactor_largeVerifier_twelfthRoot_le {eta alpha : ℝ} @@ -2769,8 +2759,6 @@ theorem unconditionalPrefactor_largeVerifier_twelfthRoot_le (large : 1 < 64 * Real.sqrt eta + alpha ^ (1 / 3 : ℝ)) : (2 : ℝ) ≤ 128 * (eta ^ (1 / 12 : ℝ) + alpha ^ (1 / 12 : ℝ)) := by - have eta_root_nonnegative : 0 ≤ eta ^ (1 / 12 : ℝ) := - Real.rpow_nonneg eta_nonnegative _ have alpha_root_nonnegative : 0 ≤ alpha ^ (1 / 12 : ℝ) := Real.rpow_nonneg alpha_positive.le _ by_cases eta_bounded : eta ≤ 1 @@ -2787,11 +2775,11 @@ theorem unconditionalPrefactor_largeVerifier_twelfthRoot_le alpha_positive.le alpha_bounded (by norm_num : (0 : ℝ) ≤ 1 / 12) (by norm_num : (1 / 12 : ℝ) ≤ 1 / 3) - linarith + linarith only [large, alpha_root_nonnegative, eta_root_compare, alpha_root_compare] · have eta_large : 1 ≤ eta := (lt_of_not_ge eta_bounded).le have eta_root_large : 1 ≤ eta ^ (1 / 12 : ℝ) := Real.one_le_rpow eta_large (by norm_num : (0 : ℝ) ≤ 1 / 12) - linarith + linarith only [alpha_root_nonnegative, eta_root_large] end @@ -2836,7 +2824,7 @@ theorem unconditionalExactSourceScalarClipping intro ξ exact (dSVDensityRationalCanonicalAcceptedTarget_distance_sq_le - (by linarith) grid ξ).trans scalar + (by linarith only [width]) grid ξ).trans scalar end @@ -3049,7 +3037,7 @@ theorem exactLocallySampleableJA_rounded_totalVariation_le _ = gamma := by rw [← Finset.sum_mul, localQuestionWeight_sum G n D remaining] - ring + ac_rfl theorem exactLocallySampleableJB_rounded_totalVariation_le (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) @@ -3108,7 +3096,7 @@ theorem exactLocallySampleableJB_rounded_totalVariation_le _ = gamma := by rw [← Finset.sum_mul, localQuestionWeight_sum G n D remaining] - ring + ac_rfl theorem exactLocallySampleableRounded_pair_totalVariation (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) @@ -3236,7 +3224,7 @@ theorem exactLocallySampleablePermutationMismatch_le_two_tv rw [Finset.mul_sum] apply Finset.sum_congr rfl intro c _ - ring + ac_rfl _ = 2 * finiteTotalVariation (exactLocallySampleableJARounded G n D denominator numerator) @@ -3819,7 +3807,7 @@ private theorem finiteProductMarginal_relativeEntropy_le hp (finiteIndependentProductWeight_nonneg marginal hm_nonnegative) change (∑ i : ι, finiteRelativeEntropy (marginal i) (q i)) ≤ _ - linarith + linarith only [hnonnegative] end @@ -3884,7 +3872,7 @@ theorem exactIndependentCoordinateQuestion_marginal rw [Finset.sum_mul] apply Finset.sum_congr rfl intro seed _ - split_ifs <;> simp + split_ifs <;> simp only [zero_mul] _ = (1 / (Fintype.card M : ℝ)) * coordinateMass := by rw [exactSeedWeight_coordinate_marginal i] @@ -3909,7 +3897,7 @@ theorem strategyAliceQuestionPrior_marginal intro y _ simp_rw [← Finset.mul_sum] rw [S.outcomeProbability_normalized x y] - ring + ac_rfl theorem strategyBobQuestionPrior_marginal (G : Game X Y A B) (S : Strategy G) (y : Y) : @@ -3932,7 +3920,7 @@ theorem strategyBobQuestionPrior_marginal intro x _ simp_rw [← Finset.mul_sum] rw [S.outcomeProbability_normalized x y] - ring + ac_rfl private theorem repeatedAliceQuestionPrior_product (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) @@ -5208,7 +5196,7 @@ theorem finiteSupportedConditionalHistoryReferenceFirstMarginal_eq field_simp [hqi] _ = jointFirstMarginal (jointConditional p i) r := by rw [← Finset.mul_sum, reference_normalized i supported r] - ring + ac_rfl theorem finiteSupportedConditionalHistoryReferenceConditional_eq {I R V : Type*} [Fintype R] [Fintype V] @@ -6242,6 +6230,14 @@ theorem exactConditionedAnswerFlag_eq_of_history (fun r : ExactHistoryFlag X Y A B D => r.bobAnswer) same_history +private theorem finitePrefixMask_attach_flag + {C F V : Type*} {m : ℕ} + (default : V) (marker : Fin (m + 1)) + (point : C × (Fin m → V)) (flag : F) : + finitePrefixMask default marker ((point.1, flag), point.2) = + (((finitePrefixMask default marker point).1, flag), + (finitePrefixMask default marker point).2) := rfl + theorem exactReverseAliceMarkedHistoryContext_eq_of_history (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (default : Y) @@ -6259,52 +6255,12 @@ theorem exactReverseAliceMarkedHistoryContext_eq_of_history G n S D default seed outcome' := by have hmask := exactReverseAliceMaskedProjection_eq_of_history (X := X) (Y := Y) (A := A) (B := B) - D default (seed, outcome) (seed, outcome') - same_history same_question + D default (seed, outcome) (seed, outcome') same_history same_question have hflag := exactConditionedAnswerFlag_eq_of_history G n S D (seed, outcome) (seed, outcome') same_history - have hfixed : - (exactReverseAliceSourceProjection - (X := X) (Y := Y) (A := A) (B := B) - D (exactReverseLeftSide seed) (seed, outcome)).1 = - (exactReverseAliceSourceProjection - (X := X) (Y := Y) (A := A) (B := B) - D (exactReverseLeftSide seed) (seed, outcome')).1 := by - have h := congrArg - (fun t : - ExactReverseAliceFixedInformation X Y D - (exactReverseLeftSide seed) × - (Fin (exactReverseLeftSide seed).card → Y) => - t.1) hmask - simpa only [finitePrefixMask] using h - have hprefix : - (finitePrefixMask default - ((exactReverseAliceContext seed).sideRank - ⟨seed.coordinate, - exactReverseLeftSide_coordinate_mem seed⟩).castSucc - (exactReverseAliceSourceProjection - (X := X) (Y := Y) (A := A) (B := B) - D (exactReverseLeftSide seed) (seed, outcome))).2 = - (finitePrefixMask default - ((exactReverseAliceContext seed).sideRank - ⟨seed.coordinate, - exactReverseLeftSide_coordinate_mem seed⟩).castSucc - (exactReverseAliceSourceProjection - (X := X) (Y := Y) (A := A) (B := B) - D (exactReverseLeftSide seed) (seed, outcome'))).2 := by - exact congrArg - (fun t : - ExactReverseAliceFixedInformation X Y D - (exactReverseLeftSide seed) × - (Fin (exactReverseLeftSide seed).card → Y) => - t.2) hmask unfold exactReverseAliceMarkedHistoryContext - dsimp - apply Prod.ext - · apply Prod.ext - · exact hfixed - · exact hflag - · exact hprefix + dsimp only + rw [finitePrefixMask_attach_flag, finitePrefixMask_attach_flag, hmask, hflag] theorem exactReverseBobMarkedHistoryContext_eq_of_history (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) @@ -6323,52 +6279,12 @@ theorem exactReverseBobMarkedHistoryContext_eq_of_history G n S D default seed outcome' := by have hmask := exactReverseBobMaskedProjection_eq_of_history (X := X) (Y := Y) (A := A) (B := B) - D default (seed, outcome) (seed, outcome') - same_history same_question + D default (seed, outcome) (seed, outcome') same_history same_question have hflag := exactConditionedAnswerFlag_eq_of_history G n S D (seed, outcome) (seed, outcome') same_history - have hfixed : - (exactReverseBobSourceProjection - (X := X) (Y := Y) (A := A) (B := B) - D (exactReverseRightSide seed) (seed, outcome)).1 = - (exactReverseBobSourceProjection - (X := X) (Y := Y) (A := A) (B := B) - D (exactReverseRightSide seed) (seed, outcome')).1 := by - have h := congrArg - (fun t : - ExactReverseBobFixedInformation X Y D - (exactReverseRightSide seed) × - (Fin (exactReverseRightSide seed).card → X) => - t.1) hmask - simpa only [finitePrefixMask] using h - have hprefix : - (finitePrefixMask default - ((exactReverseBobContext seed).sideRank - ⟨seed.coordinate, - exactReverseRightSide_coordinate_mem seed⟩).castSucc - (exactReverseBobSourceProjection - (X := X) (Y := Y) (A := A) (B := B) - D (exactReverseRightSide seed) (seed, outcome))).2 = - (finitePrefixMask default - ((exactReverseBobContext seed).sideRank - ⟨seed.coordinate, - exactReverseRightSide_coordinate_mem seed⟩).castSucc - (exactReverseBobSourceProjection - (X := X) (Y := Y) (A := A) (B := B) - D (exactReverseRightSide seed) (seed, outcome'))).2 := by - exact congrArg - (fun t : - ExactReverseBobFixedInformation X Y D - (exactReverseRightSide seed) × - (Fin (exactReverseRightSide seed).card → X) => - t.2) hmask unfold exactReverseBobMarkedHistoryContext - dsimp - apply Prod.ext - · apply Prod.ext - · exact hfixed - · exact hflag - · exact hprefix + dsimp only + rw [finitePrefixMask_attach_flag, finitePrefixMask_attach_flag, hmask, hflag] theorem exactReverseAlice_history_of_marked_context (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) @@ -6906,7 +6822,7 @@ theorem reweightedSeedPrefixPrior_as_flagged_pushforward groupedMass projection (reweightedSeedPriorEventLaw seedLaw G n S).weight (t.1.1, t.2) := by - ring + ac_rfl _ = groupedMass (fun q : ConditionedAnswerFlag A B D × (K × ExactOutcome X Y A B n) => @@ -7044,29 +6960,7 @@ theorem finiteGroupedExpectation_eq_atom_sum (code : Ω → C) (mass : Ω → ℝ) (value : C → ℝ) : (∑ target : C, groupedMass code mass target * value target) = ∑ outcome : Ω, mass outcome * value (code outcome) := by - classical - unfold groupedMass - calc - (∑ target : C, - (∑ outcome ∈ - (Finset.univ.filter fun outcome : Ω => - code outcome = target), mass outcome) * value target) = - ∑ target : C, - ∑ outcome ∈ - (Finset.univ.filter fun outcome : Ω => - code outcome = target), - mass outcome * value (code outcome) := by - apply Finset.sum_congr rfl - intro target _ - rw [Finset.sum_mul] - apply Finset.sum_congr rfl - intro outcome houtcome - have hcode : code outcome = target := - (Finset.mem_filter.mp houtcome).2 - rw [hcode] - _ = ∑ outcome : Ω, mass outcome * value (code outcome) := - Finset.sum_fiberwise Finset.univ code - (fun outcome => mass outcome * value (code outcome)) + exact groupedMass_expectation code mass value theorem jointFirstMarginal_groupedContextNext {Ω C V : Type*} [Fintype Ω] [Fintype V] diff --git a/LeanPool/QuantumParallelRepetition/Part08.lean b/LeanPool/QuantumParallelRepetition/Part08.lean index c8eb495dc3..bffe088d81 100644 --- a/LeanPool/QuantumParallelRepetition/Part08.lean +++ b/LeanPool/QuantumParallelRepetition/Part08.lean @@ -531,7 +531,7 @@ theorem existsCommonSupportPreservingRationalApproximations denominator_large have crossed := (div_lt_iff₀ gamma_positive).mp reciprocal_bound - linarith + linarith only [crossed] refine ⟨denominator, denominator_positive, fun index => distributionRoundedNumerator base denominator (probability index), ?_, ?_, ?_⟩ @@ -598,7 +598,7 @@ theorem existsCommonSupportPreservingRationalApproximations have crossed := (div_lt_iff₀ genuinely_positive).mp reciprocal_lt_denominator - linarith + linarith only [crossed] have positive_floor : 0 < distributionFloorNumerator denominator (probability index) letter := by @@ -1058,7 +1058,7 @@ private theorem exactSourceConditionalWinningProbability_mul_law rw [zero] at bounded have accepted_zero : exactSourceAcceptedCoordinateMass G n S D t = 0 := by - linarith + linarith only [nonnegative, bounded] simp only [zero, zero_mul, accepted_zero] · unfold exactSourceConditionalWinningProbability field_simp [zero] @@ -1162,7 +1162,7 @@ private theorem exactSourceAcceptedCoordinateMass_sum_eq_remaining_average intro outcome _ apply Finset.sum_congr rfl intro seed _ - split <;> simp + split <;> simp only [mul_zero] _ = ∑ outcome : ExactOutcome X Y A B n, ∑ i : SourceRemainingCoordinate D, (1 / (Fintype.card (SourceRemainingCoordinate D) : ℝ)) * @@ -1245,7 +1245,7 @@ theorem exactSource_failure_sum_lt_of_uniform rw [← Finset.sum_div] at failure have first := (div_lt_iff₀ cardinality).mp failure have second := (div_lt_iff₀ positive).mp first - linarith + linarith only [second] theorem exactSourceConditionalWinningProbability_gt_of_uniform_failure (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) @@ -1584,7 +1584,7 @@ private theorem exactSourceConditionalWinningProbability_eq_fine_born_ratio rw [exactLocallySampleableLaw_eq_fair_born, ite_eq_left accepted, exactFairFullOutcomeBornMass_eq_reveal_question_norm] - ring + ac_rfl unfold exactSourceConditionalWinningProbability rw [exactSourceAcceptedCoordinateMass_eq_seeded_fair_born G n S D positive history x y, ite_eq_left accepted, posterior] @@ -2089,7 +2089,7 @@ theorem exactLocallySampleableLaw_fiber_ne_zero_of_ne_zero exactSeedWeight t.2.2.2.seed * (exactRevealMass G n D t.2.2.2.seed t.2.2.2.history * - G.questionWeight t.2.1 t.2.2.1) by ring] + G.questionWeight t.2.1 t.2.2.1) by ac_rfl] simp only [reveal_zero, mul_zero, zero_mul, zero_div] theorem exactLocallySampleableLaw_psi_ne_zero_of_ne_zero @@ -2905,7 +2905,7 @@ theorem exactStrategyQuestionCodeGroupedMass rw [Finset.mul_sum] _ = (G.repeat n).questionWeight xs ys := by rw [S.outcomeProbability_normalized xs ys] - ring + ac_rfl · simp only [compatible, ↓reduceIte, sum_const_zero] theorem exactRepeatedQuestionWeight_splitAt_bob @@ -2926,8 +2926,7 @@ theorem exactRepeatedQuestionWeight_splitAt_bob G.questionWeight (xs j) ((Equiv.funSplitAt i Y).symm (y, tail) j)) (Finset.mem_univ i)] - simp only [ne_eq, Equiv.funSplitAt, Equiv.piSplitAt, eq_rec_constant, Equiv.symm_mk, - Equiv.coe_fn_mk, ↓reduceDIte] + simp only [ne_eq, Equiv.funSplitAt_symm_apply, ↓reduceDIte] theorem exactRepeatedQuestionTail_splitAt_bob (G : Game X Y A B) (n : ℕ) @@ -2943,8 +2942,7 @@ theorem exactRepeatedQuestionTail_splitAt_bob apply Finset.prod_congr rfl intro j hj have different : j ≠ i := (Finset.mem_erase.mp hj).1 - simp only [ne_eq, Equiv.funSplitAt, Equiv.piSplitAt, eq_rec_constant, Equiv.symm_mk, - Equiv.coe_fn_mk, different, ↓reduceDIte] + simp only [ne_eq, Equiv.funSplitAt_symm_apply, different, ↓reduceDIte] end @@ -3032,8 +3030,7 @@ theorem exactStrategyStableBobQuestionCode_joint_factor · have hx : xs coordinate = question := determines xs (split.symm (next, tail)) compatible have marked (y : Y) : split.symm (y, tail) coordinate = y := by - simp only [ne_eq, Equiv.funSplitAt, Equiv.piSplitAt, eq_rec_constant, Equiv.symm_mk, - Equiv.coe_fn_mk, ↓reduceDIte, split] + simp only [ne_eq, Equiv.funSplitAt_symm_apply, ↓reduceDIte, split] simp_rw [same_code, marked] simp only [compatible, Prod.mk.injEq, true_and, ↓reduceIte] simp only [Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte] @@ -3060,7 +3057,7 @@ theorem exactStrategyStableBobQuestionCode_joint_factor (G.marginalX (xs coordinate) * _) rw [hx] rw [← G.marginalX_mul_conditionalYGivenX question next] - ring + ac_rfl · simp_rw [same_code] simp only [ne_eq, Prod.mk.injEq, compatible, false_and, ↓reduceIte, sum_const_zero, mul_zero] @@ -3084,8 +3081,7 @@ theorem exactRepeatedQuestionWeight_splitAt_alice ((Equiv.funSplitAt coordinate X).symm (x, tail) j) (ys j)) (Finset.mem_univ coordinate)] - simp only [ne_eq, Equiv.funSplitAt, Equiv.piSplitAt, eq_rec_constant, Equiv.symm_mk, - Equiv.coe_fn_mk, ↓reduceDIte] + simp only [ne_eq, Equiv.funSplitAt_symm_apply, ↓reduceDIte] theorem exactRepeatedQuestionTail_splitAt_alice (G : Game X Y A B) (n : ℕ) @@ -3103,8 +3099,7 @@ theorem exactRepeatedQuestionTail_splitAt_alice apply Finset.prod_congr rfl intro j hj have different : j ≠ coordinate := (Finset.mem_erase.mp hj).1 - simp only [ne_eq, Equiv.funSplitAt, Equiv.piSplitAt, eq_rec_constant, Equiv.symm_mk, - Equiv.coe_fn_mk, different, ↓reduceDIte] + simp only [ne_eq, Equiv.funSplitAt_symm_apply, different, ↓reduceDIte] theorem exactStrategyStableAliceQuestionCode_joint_factor {C : Type*} [DecidableEq C] @@ -3182,8 +3177,7 @@ theorem exactStrategyStableAliceQuestionCode_joint_factor · have hy : ys coordinate = question := determines (split.symm (next, tail)) ys compatible have marked (x : X) : split.symm (x, tail) coordinate = x := by - simp only [ne_eq, Equiv.funSplitAt, Equiv.piSplitAt, eq_rec_constant, Equiv.symm_mk, - Equiv.coe_fn_mk, ↓reduceDIte, split] + simp only [ne_eq, Equiv.funSplitAt_symm_apply, ↓reduceDIte, split] simp_rw [same_code, marked] simp only [compatible, Prod.mk.injEq, true_and, ↓reduceIte] simp only [Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte] @@ -3210,7 +3204,7 @@ theorem exactStrategyStableAliceQuestionCode_joint_factor (G.marginalY (ys coordinate) * _) rw [hy] rw [← G.marginalY_mul_conditionalXGivenY next question] - ring + ac_rfl · simp_rw [same_code] simp only [ne_eq, Prod.mk.injEq, compatible, false_and, ↓reduceIte, sum_const_zero, mul_zero] @@ -4312,7 +4306,7 @@ theorem groupedMass_flagSeedOutcome_reassoc (if code point.1.1 point.1.2 point.2 = target then flagWeight point.1.1 * (seedWeight point.1.2 * outcomeWeight point.2) else 0) - split <;> simp [mul_assoc] + split <;> simp only [mul_assoc] variable {X Y A B : Type*} variable [Fintype X] [Fintype Y] [Fintype A] [Fintype B] @@ -4393,7 +4387,7 @@ theorem mixedStableBobQuestionCode_joint_factor rw [Finset.mul_sum] apply Finset.sum_congr rfl intro index _ - ring + ac_rfl _ = G.conditionalYGivenX question next * groupedMass (fun point : K × ExactOutcome X Y A B n => @@ -4484,7 +4478,7 @@ theorem mixedStableAliceQuestionCode_joint_factor rw [Finset.mul_sum] apply Finset.sum_congr rfl intro index _ - ring + ac_rfl _ = G.conditionalXGivenY question next * groupedMass (fun point : K × ExactOutcome X Y A B n => @@ -4593,8 +4587,7 @@ private theorem exactReverseAliceMaskedQuestionRegister_stable have different : j.val ≠ coordinate := by intro same exact outsideD (same ▸ j.property) - simp only [ne_eq, Equiv.funSplitAt, Equiv.piSplitAt, eq_rec_constant, Equiv.symm_mk, - Equiv.coe_fn_mk, different, ↓reduceDIte] + simp only [ne_eq, Equiv.funSplitAt_symm_apply, different, ↓reduceDIte] apply Prod.ext · rfl apply Prod.ext @@ -4606,8 +4599,7 @@ private theorem exactReverseAliceMaskedQuestionRegister_stable apply Subtype.ext exact same exact actual ▸ j.property - simp only [ne_eq, Equiv.funSplitAt, Equiv.piSplitAt, eq_rec_constant, Equiv.symm_mk, - Equiv.coe_fn_mk, different, ↓reduceDIte] + simp only [ne_eq, Equiv.funSplitAt_symm_apply, different, ↓reduceDIte] · rfl · rfl · funext position @@ -4625,8 +4617,8 @@ private theorem exactReverseAliceMaskedQuestionRegister_stable context.sideRank.symm.injective sameMarked exact (Nat.ne_of_lt before) (congrArg Fin.val samePosition) - simp only [Fin.val_castSucc, before, ↓reduceIte, ne_eq, Equiv.funSplitAt, Equiv.piSplitAt, - eq_rec_constant, Equiv.symm_mk, Equiv.coe_fn_mk, different, ↓reduceDIte, context] + simp only [Fin.val_castSucc, before, ↓reduceIte, ne_eq, Equiv.funSplitAt_symm_apply, + different, ↓reduceDIte, context] · simp only [Fin.val_castSucc, before, ↓reduceIte] private theorem exactConditionedReverseAliceNextPrior_flagged_mixture @@ -5456,7 +5448,7 @@ private theorem exactReverseAlicePrefixIncrement_eq_contextMarkerInformation repeatedConditionedOutcomeLaw G n S D outcome) * _ = law.weight seed * (repeatedConditionedOutcomeLaw G n S D outcome * _) - ring + ac_rfl private theorem exactReverseAlicePrefixInformation_eq_seedMarkerAverage (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) @@ -5708,7 +5700,7 @@ private theorem exactAliceSourceConditionalInformation_eq_seedBornAverage apply Finset.sum_congr rfl intro outcome _ unfold exactPostselectedJointLaw - ring + ac_rfl theorem exactReverseAliceConditionalHistoryIdentification_proved (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) @@ -5798,8 +5790,7 @@ private theorem exactReverseBobMaskedQuestionRegister_stable have different : j.val ≠ coordinate := by intro same exact outsideD (same ▸ j.property) - simp only [ne_eq, Equiv.funSplitAt, Equiv.piSplitAt, eq_rec_constant, Equiv.symm_mk, - Equiv.coe_fn_mk, different, ↓reduceDIte] + simp only [ne_eq, Equiv.funSplitAt_symm_apply, different, ↓reduceDIte] apply Prod.ext · rfl apply Prod.ext @@ -5813,8 +5804,7 @@ private theorem exactReverseBobMaskedQuestionRegister_stable apply Subtype.ext exact same exact actual ▸ j.property - simp only [ne_eq, Equiv.funSplitAt, Equiv.piSplitAt, eq_rec_constant, Equiv.symm_mk, - Equiv.coe_fn_mk, different, ↓reduceDIte] + simp only [ne_eq, Equiv.funSplitAt_symm_apply, different, ↓reduceDIte] · rfl · rfl · funext position @@ -5832,8 +5822,8 @@ private theorem exactReverseBobMaskedQuestionRegister_stable context.sideRank.symm.injective sameMarked exact (Nat.ne_of_lt before) (congrArg Fin.val samePosition) - simp only [Fin.val_castSucc, before, ↓reduceIte, ne_eq, Equiv.funSplitAt, Equiv.piSplitAt, - eq_rec_constant, Equiv.symm_mk, Equiv.coe_fn_mk, different, ↓reduceDIte, context] + simp only [Fin.val_castSucc, before, ↓reduceIte, ne_eq, Equiv.funSplitAt_symm_apply, + different, ↓reduceDIte, context] · simp only [Fin.val_castSucc, before, ↓reduceIte] private theorem exactConditionedReverseBobNextPrior_flagged_mixture @@ -6559,7 +6549,7 @@ private theorem exactConditionedReverseBobPrefixEntropyIncrement_eq_markedOutcom (repeatedConditionedOutcomeLaw G n S D outcome * exactReverseBobActualMarkedEntropyScore G n S D remaining default side seed marker outcome) - ring + ac_rfl private theorem exactConditionedReverseBobPrefixInformation_eq_sourceMarkerAverage (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) @@ -6774,7 +6764,7 @@ theorem exactReverseBobConditionalHistoryIdentification_proved · rw [exactReverseBobActualMarkedEntropy_eq_source G n S D remaining positive default seed outcome zero] unfold exactPostselectedJointLaw - ring + ac_rfl end @@ -6961,7 +6951,7 @@ theorem exact_source_equation_twenty_seven_support_preserving G n D denominator numerator) (exactLocallySampleableLaw G n S D)] _ ≤ 4 * (kappa + gamma) := by - linarith + linarith only [rounded_alice, rounded_bob] theorem exact_source_equation_twenty_seven_support_preserving_of_information diff --git a/LeanPool/QuantumParallelRepetition/Part09.lean b/LeanPool/QuantumParallelRepetition/Part09.lean index db15a7af95..4ed86c8a02 100644 --- a/LeanPool/QuantumParallelRepetition/Part09.lean +++ b/LeanPool/QuantumParallelRepetition/Part09.lean @@ -38,7 +38,7 @@ theorem gameQuestionX_nonempty apply Finset.sum_eq_zero intro x _ exact (empty ⟨x⟩).elim - linarith [G.weight_normalized] + linarith only [zero, G.weight_normalized] theorem gameQuestionY_nonempty (G : Game X Y A B) : Nonempty Y := by @@ -133,12 +133,12 @@ theorem exact_totalSamplingLoss_mono (32 * η₂) ^ (1 / 12 : ℝ) := by apply Real.rpow_le_rpow · positivity - · linarith + · linarith only [eta_le] · norm_num have eta_sqrt : Real.sqrt (8 * η₁) ≤ Real.sqrt (8 * η₂) := by apply Real.sqrt_le_sqrt - linarith + linarith only [eta_le] unfold totalSamplingLoss gcongr @@ -153,9 +153,6 @@ theorem exact_standardQuantumParallelRepetition_of_source_rounding no_exponential_bound obtain ⟨K₀, constant_nonnegative, construct⟩ := rounding let gapValue : ℝ := 1 - entangledValue G - have gap_positive : 0 < gapValue := by - dsimp [gapValue] - linarith let failureTolerance : ℝ := min (gapValue / 2) (1 / 2) have failure_positive : 0 < failureTolerance := by dsimp [failureTolerance] @@ -163,7 +160,7 @@ theorem exact_standardQuantumParallelRepetition_of_source_rounding have failure_at_most_one : failureTolerance ≤ 1 := by have half := min_le_right (gapValue / 2) (1 / 2 : ℝ) dsimp [failureTolerance] - linarith + linarith only [failure_positive, half] let rate : ℕ → ℝ := fun k => 1 / ((k : ℝ) + 1) have rate_positive (k : ℕ) : 0 < rate k := by dsimp [rate] @@ -171,8 +168,7 @@ theorem exact_standardQuantumParallelRepetition_of_source_rounding have rate_at_most_one (k : ℕ) : rate k ≤ 1 := by dsimp [rate] apply (div_le_iff₀ (by positivity : (0 : ℝ) < (k : ℝ) + 1)).2 - have nonnegative : (0 : ℝ) ≤ (k : ℝ) := by positivity - linarith + linarith only [] have rate_tendsto : Tendsto rate atTop (𝓝 0) := by exact tendsto_one_div_add_atTop_nhds_zero_nat have martingale_tendsto : @@ -220,7 +216,7 @@ theorem exact_standardQuantumParallelRepetition_of_source_rounding apply exact_totalSamplingLoss_mono constant_nonnegative (rate_positive k).le (le_refl _) martingale_nonnegative martingale_small - linarith + linarith only [pinsker_small] exact source_equation_twenty_nine_contradiction G rounded K₀ (rate k) (martingaleRate G n S D) (exactSourcePinskerRate G n S D + rate k) @@ -345,7 +341,7 @@ theorem residualIdentity_quadratic apply Finset.sum_congr rfl intro k _ simp only [star_mul] - ring + ac_rfl _ = ∑ i : s, (∑ j : s, M i j * z j) * star (z i) := by rw [residual_complex] simp only [RCLike.star_def, mul_one] @@ -738,10 +734,9 @@ theorem unconditionalMatchedVerifierTensor_norm ‖target‖ * ‖work‖ := by have squared := unconditionalMatchedVerifierTensor_norm_sq target work - nlinarith [ - norm_nonneg (unconditionalMatchedVerifierTensor target work), - norm_nonneg target, norm_nonneg work, - mul_nonneg (norm_nonneg target) (norm_nonneg work)] + exact (sq_eq_sq₀ (norm_nonneg _) + (mul_nonneg (norm_nonneg target) (norm_nonneg work))).mp (by + simpa only [mul_pow] using squared) theorem unconditionalMatchedVerifierEffect_tensor_complement {s t : Type*} [DecidableEq s] [DecidableEq t] @@ -856,7 +851,7 @@ theorem unconditionalMatchedVerifierEffect_tensor_quadratic apply Finset.sum_congr rfl intro k _ simp only [star_mul] - ring + ac_rfl _ = (∑ i : s, (∑ j : s, effect i j * target j) * star (target i)) * (↑(‖work‖ ^ 2) : ℂ) := by @@ -1044,10 +1039,10 @@ theorem unconditionalSelectedCopy_weightedAffine congr 1 apply Finset.sum_congr rfl intro i _ - ring + ac_rfl _ = coefficient * (∑ i, weight i * asynchronous i) + residual := by rw [normalized] - ring + ac_rfl end @@ -1143,28 +1138,12 @@ theorem unconditionalMatchedVerifierAggregate_dependent_le |(∑ j : J, weight j * quadraticExpectation (effect j) (actual j)) - (∑ j : J, weight j * quadraticExpectation (effect j) (ideal j))| ≤ 2 * Real.sqrt Δ := by - have actual_nonnegative : - 0 ≤ ∑ j : J, weight j * ‖actual j‖ ^ 2 := - Finset.sum_nonneg - (fun j _ => mul_nonneg (nonnegative j) (sq_nonneg _)) - have ideal_nonnegative : - 0 ≤ ∑ j : J, weight j * ‖ideal j‖ ^ 2 := - Finset.sum_nonneg - (fun j _ => mul_nonneg (nonnegative j) (sq_nonneg _)) - have error_nonnegative : - 0 ≤ ∑ j : J, weight j * ‖actual j - ideal j‖ ^ 2 := - Finset.sum_nonneg - (fun j _ => mul_nonneg (nonnegative j) (sq_nonneg _)) have actual_root : - Real.sqrt (∑ j : J, weight j * ‖actual j‖ ^ 2) ≤ 1 := by - nlinarith [ - Real.sq_sqrt actual_nonnegative, - Real.sqrt_nonneg (∑ j : J, weight j * ‖actual j‖ ^ 2)] + Real.sqrt (∑ j : J, weight j * ‖actual j‖ ^ 2) ≤ 1 := + Real.sqrt_le_one.mpr actual_mass have ideal_root : - Real.sqrt (∑ j : J, weight j * ‖ideal j‖ ^ 2) ≤ 1 := by - nlinarith [ - Real.sq_sqrt ideal_nonnegative, - Real.sqrt_nonneg (∑ j : J, weight j * ‖ideal j‖ ^ 2)] + Real.sqrt (∑ j : J, weight j * ‖ideal j‖ ^ 2) ≤ 1 := + Real.sqrt_le_one.mpr ideal_mass calc |(∑ j : J, weight j * quadraticExpectation (effect j) (actual j)) - (∑ j : J, weight j * quadraticExpectation (effect j) (ideal j))| ≤ @@ -1175,7 +1154,7 @@ theorem unconditionalMatchedVerifierAggregate_dependent_le weight nonnegative effect contraction actual ideal _ ≤ 2 * Real.sqrt Δ := by apply mul_le_mul - · linarith + · linarith only [actual_root, ideal_root] · exact Real.sqrt_le_sqrt deviation · exact Real.sqrt_nonneg _ · norm_num @@ -1213,8 +1192,7 @@ theorem unconditionalConjugatePureVector_norm {ι : Type*} [Fintype ι] (z : EuclideanSpace ℂ ι) : ‖unconditionalConjugatePureVector z‖ = ‖z‖ := by have squares := unconditionalConjugatePureVector_norm_sq z - nlinarith [norm_nonneg (unconditionalConjugatePureVector z), - norm_nonneg z] + exact (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp squares /-- Transpose every effect of a POVM to obtain the conjugate measurement. -/ def unconditionalConjugatePOVM @@ -1247,7 +1225,7 @@ theorem unconditionalConjugatePureVector_transpose_quadratic intro i _ apply Finset.sum_congr rfl intro j _ - ring + ac_rfl private theorem unconditionalConjugatePOVM_jointEffect {A B ι κ : Type*} [Fintype A] [Fintype B] @@ -1446,19 +1424,6 @@ theorem unconditionalCanonicalAcceptedCoefficient_sourceScale ((dSVDensityRationalPhysicalAcceptedRank w N ξ i).val : ℝ) = dSVDensityRationalCanonicalAcceptedCoefficient w N ξ i := by - have d_nonzero : (d : ℝ) ≠ 0 := by - exact_mod_cast (Nat.ne_of_gt dimension) - have n_nonzero : (N : ℝ) ≠ 0 := by - exact_mod_cast (Nat.ne_of_gt grid) - have source_positive : - 0 < ‖sharedThresholdResourceRaw (d := Fin d) - (fun _ : Fin N => (1 : ℝ))‖ := by - have source_sq := dSVUniformDensityThresholdRaw_norm_sq N d - have product_positive : (0 : ℝ) < (d : ℝ) * (N : ℝ) := by - positivity - nlinarith [norm_nonneg - (sharedThresholdResourceRaw (d := Fin d) - (fun _ : Fin N => (1 : ℝ)))] have left_nonnegative : 0 ≤ Real.sqrt (w * (d : ℝ)) * (‖sharedThresholdResourceRaw (d := Fin d) @@ -1489,7 +1454,7 @@ theorem unconditionalCanonicalAcceptedCoefficient_sourceScale dSVDensityRationalPhysicalAcceptedRank_targetCoefficient_sq width N ξ i] field_simp - nlinarith + exact (sq_eq_sq₀ left_nonnegative right_nonnegative).mp same_square theorem unconditionalConjugateTranspose_eq_inverse {d : ℕ} (U : Matrix.unitaryGroup (Fin d) ℂ) : @@ -1624,7 +1589,7 @@ theorem unconditionalMixedConjugateCanonicalAcceptedTarget_sum rw [Finset.mul_sum] apply Finset.sum_congr rfl intro j _ - ring + ac_rfl _ = ∑ i : Fin d, (dSVDensityRationalCanonicalAcceptedCoefficient @@ -1644,7 +1609,7 @@ theorem unconditionalMixedConjugateCanonicalAcceptedTarget_sum push_cast at coefficient rw [← coefficient] push_cast - ring + ac_rfl _ = _ := (unconditionalConjugateCanonicalAcceptedTarget_apply w ξ a b).symm @@ -1703,8 +1668,10 @@ theorem unconditionalMixedConjugateSigmaAtomLift_apply classical by_cases phase : φ = ψ <;> by_cases work : a = b <;> - simp [unconditionalMixedConjugateSigmaAtomLift, - Matrix.reindex_apply, Matrix.kroneckerMap_apply, phase, work] + simp only [unconditionalMixedConjugateSigmaAtomLift, reindex_apply, Equiv.symm_symm, phase, + work, submatrix_apply, Equiv.sigmaEquivProd_apply, kroneckerMap_apply, one_apply_eq, + one_mul, mul_one, and_self, ↓reduceIte, ne_eq, not_false_eq_true, one_apply_ne, mul_zero, + and_false, zero_mul, and_true] private def unconditionalMixedConjugateSigmaLocalAction {d m : ℕ} (B : ℕ) @@ -1795,7 +1762,7 @@ private theorem unconditionalMixedConjugateTargetCovariance intro k _ apply Finset.sum_congr rfl intro l _ - ring + ac_rfl end @@ -1822,8 +1789,6 @@ theorem unconditionalSelectedCopy_coherentPhaseSigma_norm_sq simp_rw [ dSVDensityRationalPublicBucketCoherentPhaseHistory_apply_norm_sq phases] - have phase_ne : (B : ℝ) ≠ 0 := by - exact_mod_cast (Nat.ne_of_gt phases) calc (∑ φ : Fin B, ∑ i : H, ∑ ψ : Fin B, ∑ j : H, (if φ = ψ then (B : ℝ)⁻¹ else 0) * @@ -1850,7 +1815,7 @@ theorem unconditionalSelectedCopy_coherentPhaseSigma_norm_sq intro i _ apply Finset.sum_congr rfl intro j _ - ring + ac_rfl _ = _ := by rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] @@ -2070,7 +2035,7 @@ theorem unconditionalMixedConjugateSelectedBranch_tensor_smul ext ⟨a, b⟩ change (c : ℂ) * (stage a * work b) = ((c : ℂ) * stage a) * work b - ring + ac_rfl private theorem unconditionalMixedConjugateSelectedBranchCovariance {S N d L B m : ℕ} {τ : Type*} [Fintype τ] [DecidableEq τ] @@ -2140,7 +2105,7 @@ theorem unconditionalPhysicalAcceptedCoherentStage_apply rw [unconditionalPhysicalAcceptedCoherentStage_eq_phaseSigma, dSVDensityRationalMixedCanonicalPrefixPhysicalAcceptedSigmaState_apply width grid] - ring + ac_rfl end @@ -2574,7 +2539,7 @@ theorem actualStoppingQuestionLocalWinningProbability_ge_matched rw [Fin.sum_univ_succ] have nonnegative := actualStoppingBranchBorn_nonneg G PA PB stopped (0 : Fin (L + 1)) 0 x y - linarith + linarith only [nonnegative] _ ≤ ∑ r : Fin (L + 1), ∑ s : Fin (L + 1), quadraticExpectation (Matrix.toEuclideanCLM (n := ι r × ι s) (𝕜 := ℂ) @@ -4201,32 +4166,36 @@ private theorem unconditionalActualPhysicalMixedAcceptedSpectralGauge_stage unconditionalActualPhysicalMixedAcceptedRawStage, Equiv.symm_apply_apply, ite_mul, mul_ite, zero_mul, mul_zero, mul_one] - simp only [UnitaryGroup.inv_val, star_apply, RCLike.star_def, ePRState, ofReal_inv, ite_mul, - zero_mul, mul_comm, mul_ite, mul_left_comm, mul_assoc, sum_ite_irrel, sum_ite_eq, mem_univ, - ↓reduceIte, sum_const_zero, dSVDensityRationalCanonicalPrefixSpectralOutcome, mulVec, - dotProduct, kroneckerMap_apply, Fintype.sum_prod_type, mul_sum] - let alice : Matrix - (DSVUniformDensityThresholdLocalIndex N d) - (DSVUniformDensityThresholdLocalIndex N d) ℂ := - dSVUniformDensityAliceHistorySpectralCopy (N := N) ξ - let bob : Matrix - (DSVUniformDensityThresholdLocalIndex N d) - (DSVUniformDensityThresholdLocalIndex N d) ℂ := - dSVUniformDensityBobHistoryCopyBasis (N := N) ζ + simp only [sum_ite_irrel, sum_ite_eq, mem_univ, ↓reduceIte, sum_const_zero] let summand : DSVUniformDensityThresholdLocalIndex N d → DSVUniformDensityThresholdLocalIndex N d → ℂ := fun x y => - (↑(Real.sqrt (B : ℝ)) : ℂ)⁻¹ * - (embezzlementState m (a, b) * - (dSVDensityRationalPhysicalAcceptedOutcome - w N ξ ζ (x, y) * - (alice ⟨k, i⟩ x * (starRingEnd ℂ) (bob y ⟨l, j⟩)))) - by_cases phases : φ = ψ - · simp only [ite_eq_left phases] - exact unconditionalActualPhysicalMixedAcceptedSpectralGauge_sum - summand - · simp only [ite_eq_right phases] + (dSVUniformDensityAliceHistorySpectralCopy (N := N) ξ : + Matrix (DSVUniformDensityThresholdLocalIndex N d) + (DSVUniformDensityThresholdLocalIndex N d) ℂ) ⟨k, i⟩ x * + (((dSVUniformDensityBobHistoryCopyBasis (N := N) ζ)⁻¹ : + Matrix.unitaryGroup (DSVUniformDensityThresholdLocalIndex N d) ℂ) : + Matrix (DSVUniformDensityThresholdLocalIndex N d) + (DSVUniformDensityThresholdLocalIndex N d) ℂ) ⟨l, j⟩ y * + dSVDensityRationalPhysicalAcceptedOutcome w N ξ ζ (x, y) + simp only [dSVDensityRationalCanonicalPrefixSpectralOutcome, + mulVec, dotProduct, kroneckerMap_apply, Fintype.sum_prod_type] + change _ = ePRState B (φ, ψ) * + (∑ x, ∑ y, summand x y) * embezzlementState m (a, b) + calc + _ = ∑ i' : Fin d, ∑ k' : Fin N, ∑ j' : Fin d, ∑ l' : Fin N, + ePRState B (φ, ψ) * summand ⟨k', i'⟩ ⟨l', j'⟩ * + embezzlementState m (a, b) := by + refine Finset.sum_congr rfl fun i' _ => Finset.sum_congr rfl fun k' _ => + Finset.sum_congr rfl fun j' _ => Finset.sum_congr rfl fun l' _ => ?_ + dsimp only [summand] + ac_rfl + _ = ePRState B (φ, ψ) * + (∑ i' : Fin d, ∑ k' : Fin N, ∑ j' : Fin d, ∑ l' : Fin N, + summand ⟨k', i'⟩ ⟨l', j'⟩) * embezzlementState m (a, b) := by + simp only [Finset.mul_sum, Finset.sum_mul] + _ = _ := by rw [unconditionalActualPhysicalMixedAcceptedSpectralGauge_sum] end @@ -4403,7 +4372,7 @@ private theorem unconditionalActualCanonicalFullSource_eq_rawSelectedStage j _ _ _ _] rw [directDSVActualStoppingSelectedHistory_sourceProduct] unfold dSVDensityRationalPhysicalAcceptedOutcome - ring + ac_rfl private theorem unconditionalActualCanonicalRawSelectedPhysicalStage_eq {B N d m : ℕ} (w : ℝ) @@ -4503,14 +4472,14 @@ theorem directDSVActualReindexedRetainedPOVMWinningEffect ext ⟨i, k⟩ ⟨j, l⟩ by_cases alice_work : (eA i).2 = (eA j).2 <;> by_cases bob_work : (eB k).2 = (eB l).2 <;> - simp [directDSVActualLocalPOVMWinningEffect, - directDSVActualReindexedRetainedPOVM, - reindexedPOVM, purificationAlicePOVM, - directDSVActualBilateralRetainedIndexEquiv, - Matrix.reindex_apply, Matrix.sum_apply, Matrix.ite_apply, - Matrix.submatrix_apply, - Matrix.kroneckerMap_apply, Matrix.one_apply, - Equiv.prodProdProdComm_apply, alice_work, bob_work] + simp only [directDSVActualLocalPOVMWinningEffect, directDSVActualReindexedRetainedPOVM, + reindexedPOVM, purificationAlicePOVM, Equiv.symm_symm, Matrix.sum_apply, Matrix.ite_apply, + kroneckerMap_apply, submatrix_apply, Matrix.one_apply, alice_work, ↓reduceIte, mul_one, + bob_work, Matrix.zero_apply, directDSVActualBilateralRetainedIndexEquiv, Equiv.symm_trans, + Equiv.prodProdProdComm_symm, Equiv.prodCongr_symm, reindex_apply, Equiv.coe_trans, + Equiv.prodCongr_apply, Function.comp_apply, Prod.map_apply, Equiv.prodProdProdComm_apply, + mul_zero, ite_self, sum_const_zero, + Prod.mk.injEq, and_false, zero_mul, and_true, and_self] theorem directDSVActualReindexedWinningEffect_quadratic {ι κ : Type*} [Fintype ι] [Fintype κ] @@ -5338,13 +5307,9 @@ theorem unconditionalClippedConjugateUnitTarget_distance_sq_le ‖gamma.val - (dSVDensityRationalCanonicalAcceptedUnitTarget width grid fine gamma).val‖ ^ 2 ≤ _ - nlinarith [ - norm_nonneg - (gamma.val - - (dSVDensityRationalCanonicalAcceptedUnitTarget - width grid fine gamma).val), - Real.sqrt_nonneg (1 / w + (d : ℝ) * w / (N : ℝ)), - Real.sq_sqrt clipping_nonnegative] + have squared := pow_le_pow_left₀ (norm_nonneg _) clipping 2 + simpa only [mul_pow, Real.sq_sqrt clipping_nonnegative, + show (2 : ℝ) ^ 2 = 4 by norm_num] using squared change ‖psi - accepted.val‖ ^ 2 ≤ _ nlinarith [norm_nonneg (psi - accepted.val), norm_nonneg (psi - gamma.val), @@ -5403,7 +5368,7 @@ theorem ring _ ≤ 2 * energy + 8 * (1 / w + (d : ℝ) * w / (N : ℝ)) := by dsimp [clip] - linarith + linarith only [energy_bound] variable {X Y A B : Type*} variable [Fintype X] [Fintype Y] [Fintype A] [Fintype B] @@ -5739,7 +5704,7 @@ theorem unconditionalPhaseCanonicalRaw_eq_norm_smul_unit star ((dSVDensityRationalCanonicalAcceptedUnitTarget width grid fine gamma).val (i, j)) at coefficient rw [coefficient] - ring + ac_rfl theorem unconditionalMatchedTensor_real_smul_work {s t : Type*} @@ -5751,7 +5716,7 @@ theorem unconditionalMatchedTensor_real_smul_work ext q change (c : ℂ) * (stage q.1 * work q.2) = stage q.1 * ((c : ℂ) * work q.2) - ring + ac_rfl theorem unconditionalPhaseCanonical_sourceScale_absorbed {d N B m : ℕ} {w : ℝ} @@ -5788,8 +5753,6 @@ theorem unconditionalPhaseCanonical_sourceScale_absorbed (dSVDensityRationalCanonicalAcceptedUnitTarget width grid fine gamma).val) (fun _ _ _ => embezzlementState m) - have real_dimension : 0 < (d : ℝ) := by - exact_mod_cast dimension have scale_positive : 0 < scale := by dsimp [scale] positivity @@ -6214,7 +6177,7 @@ theorem unconditionalActualSelectedBranchLocalAction_norm simp only [quadraticExpectation, map_one, one_apply_eq_self, inner_self_eq_norm_sq_to_K, coe_algebraMap, ← ofReal_pow, ofReal_re] change ‖toLp 2 (M.mulVec (ofLp z))‖ = ‖z‖ - nlinarith [norm_nonneg (toLp 2 (M.mulVec (ofLp z))), norm_nonneg z] + exact (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp squared theorem unconditionalActualSelectedBranchLocalAction_sub {ι τ : Type*} [Fintype ι] [DecidableEq ι] diff --git a/LeanPool/QuantumParallelRepetition/Part10.lean b/LeanPool/QuantumParallelRepetition/Part10.lean index 9843fd4a18..55adf29006 100644 --- a/LeanPool/QuantumParallelRepetition/Part10.lean +++ b/LeanPool/QuantumParallelRepetition/Part10.lean @@ -151,13 +151,13 @@ theorem unconditionalSelectedGaugeRetainedPOVMNaturality_effect rcases p with ⟨⟨φ, i⟩, k⟩ rcases q with ⟨⟨ψ, j⟩, l⟩ by_cases phase : φ = ψ <;> by_cases work : k = l <;> - simp [directDSVActualReindexedRetainedPOVM_effect, - physical8SelectedGlobalTargetWorkEquiv, - unitaryConjugatePOVM, Matrix.mul_apply, - Matrix.conjTranspose_apply, Fintype.sum_sigma, - Fintype.sum_prod_type, - unconditionalMixedConjugateSigmaAtomLift_apply, - mul_assoc, ite_and, phase, work, eq_comm] + simp only [physical8SelectedGlobalTargetWorkEquiv, unitaryConjugatePOVM, mul_assoc, phase, + work, directDSVActualReindexedRetainedPOVM_effect, Equiv.coe_fn_mk, Matrix.mul_apply, + conjTranspose_apply, RCLike.star_def, ↓reduceIte, mul_one, Prod.mk.injEq, ite_and, mul_ite, + mul_zero, ite_mul, zero_mul, Fintype.sum_sigma, eq_comm, sum_ite_irrel, sum_ite_eq', + mem_univ, sum_const_zero, Fintype.sum_prod_type, + unconditionalMixedConjugateSigmaAtomLift_apply, sum_ite_eq, and_true, and_false, map_zero, + ite_self, and_self] theorem unconditionalSelectedGaugeRetainedPOVMNaturality {C : Type} [Fintype C] @@ -580,7 +580,7 @@ theorem unconditionalWeightedClippedMatchedVerifierAndMassLoss have loss := mul_nonneg (sub_nonneg.mpr (source_row_mass i)) (sub_nonneg.mpr (win_bounded i)) - linarith + linarith only [loss] have clean_verifier_signed : (∑ i : I, weight i * ∑ k : K, @@ -609,7 +609,8 @@ theorem unconditionalWeightedClippedMatchedVerifierAndMassLoss 2 * Real.sqrt Δclean := by simpa only [same_work_mass] using ((le_abs_self _).trans clean_mass_gap) - linarith + linarith only [actual_success, ideal_payoff, clean_verifier_signed, clip_verifier_signed, + clean_mass_signed] end @@ -819,7 +820,6 @@ theorem unconditionalFairPhysicalFlaggedStoppingTransfer ExactSourceSharedFlag X Y A B D denominator × (X × Y)) : flagPhysical outcome ≤ 1 := history_born_bounded (history outcome) - have variation : Pinsker.finiteTotalVariation p q ≤ lam := by simpa only using total_variation have transferred := winning_expectation_transfer p q flagPhysical p_normalized q_normalized flagPhysical_nonnegative flagPhysical_bounded have p_nonnegative (outcome : @@ -845,7 +845,7 @@ theorem unconditionalFairPhysicalFlaggedStoppingTransfer exactSourceConditionalWinningProbability G n S D h) - bad - 4 * Real.sqrt deviation - 2 * Real.sqrt clipping ≤ ∑ outcome, q outcome * flagPhysical outcome at fair_verifier - linarith + linarith only [total_variation, mismatch, fair_win, transferred, discarded, fair_verifier] let stop := fun outcome : ExactSourceSharedFlag X Y A B D denominator × (X × Y) => ∑ j : Fin L, @@ -1006,7 +1006,7 @@ private theorem unconditionalActualLocalPOVMWinningEffect_add_losingEffect rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro b _ - split <;> simp + split <;> simp only [add_zero, zero_add] _ = (∑ a : A, PA.effect a) ⊗ₖ (∑ b : B, PB.effect b) := by ext ⟨i, j⟩ ⟨k, l⟩ @@ -1510,7 +1510,7 @@ theorem unconditionalActualFairCleanedRow_le_one have terminal := dSVDensityRationalHeterogeneousPhysicalTerminalMass_nonneg N width schedule ξ ζ - linarith + linarith only [partition, asynchronous, terminal] theorem unconditionalActualFairWeightedCleanedMass_le_one {I : Type} [Fintype I] @@ -1592,12 +1592,12 @@ theorem unconditionalActualFairWeightedStoppedSuccess intro h _ rw [dSVDensityRationalHeterogeneousPhysicalStopped_mass_partition grid dimension width schedule (ξ h) (ζ h)] - ring + ac_rfl _ = 1 := weight_normalized simp_rw [unconditionalActualFairCleanedRow_eq_stoppedSuccess phases grid dimension harmonic width width_positive schedule _ _ Q A C] - linarith + linarith only [asynchronous_bound, terminal_bound, partition] end @@ -1760,13 +1760,7 @@ theorem unconditionalActualFairSourceCanonicalVector_norm have squared := unconditionalActualFairSourceCanonicalVector_norm_sq phases grid harmonic width schedule ξ ζ ψ unit j positive fine - nlinarith [ - norm_nonneg (integratorActualC485SourceVector - (S := S) (B := B) (N := N) (d := d) (L := L) (m := m) - width schedule ξ ζ ψ j), - norm_nonneg (integratorActualC485CanonicalVector - (S := S) (B := B) (N := N) (d := d) (L := L) (m := m) - (width := width) schedule ξ ζ j positive grid fine)] + exact (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp squared end @@ -1881,7 +1875,7 @@ theorem unconditionalSourcePhysicalSameGridWeightedStoppingLedger 4 * rho ^ 2 + (16 * (Real.exp 1 - 1) + 4) * t) := by classical - have w_nonnegative : 0 ≤ w := by linarith + have w_nonnegative : 0 ≤ w := by linarith only [large] obtain ⟨L, horizon_positive, tail⟩ := dSVDensityRationalHeterogeneousPhysical_exists_positive_horizon dimension w_nonnegative precision @@ -1903,10 +1897,10 @@ theorem unconditionalSourcePhysicalSameGridWeightedStoppingLedger intro s have denominator : 0 < 2 * (width s + 1) := by dsimp [width] - linarith + linarith only [large] apply (le_div_iff₀ denominator).mpr dsimp [width] - linarith [grid_budget, bounded] + linarith only [bounded, grid_budget] have asynchronous (i : ι) : dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule (ξ i) (ζ i) ≤ @@ -1917,7 +1911,7 @@ theorem unconditionalSourcePhysicalSameGridWeightedStoppingLedger dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass_le_targetDistance grid dimension width width_large fine upper w_nonnegative schedule (ξ i) (ζ i) - _ ≤ _ := by linarith + _ ≤ _ := by linarith only [grid_budget] have terminal (i : ι) : dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule (ξ i) (ζ i) ≤ δ ^ 2 := @@ -1960,7 +1954,7 @@ theorem unconditionalSourcePhysicalSameGridWeightedStoppingLedger have actual := selected width schedule (ξ i) (ζ i) rw [dSVDensityRationalHeterogeneousActualAsynchronousFlagMass_eq_stoppedAsynchronousMass grid dimension width schedule (ξ i) (ζ i)] at actual - linarith + linarith only [actual] have mean_hazard := unconditionalSelectedCopy_weightedAffine weight @@ -1978,7 +1972,7 @@ theorem unconditionalSourcePhysicalSameGridWeightedStoppingLedger refine ⟨asynchronous, terminal, mean_asynchronous, mean_terminal, ?_⟩ have scaled := mul_le_mul_of_nonneg_left mean_asynchronous (show 0 ≤ (34 : ℝ) / t by positivity) - linarith + linarith only [mean_hazard, scaled] end @@ -1992,9 +1986,10 @@ private theorem unconditionalSmallSource_eta_le_one eta ≤ 1 := by have delta_nonnegative : 0 ≤ alpha ^ (1 / 3 : ℝ) := Real.rpow_nonneg alpha_positive.le _ - have root_nonnegative := Real.sqrt_nonneg eta - have root_square := Real.sq_sqrt eta_nonnegative - nlinarith + calc + eta = Real.sqrt eta ^ 2 := (Real.sq_sqrt eta_nonnegative).symm + _ ≤ 1 := pow_le_one₀ (Real.sqrt_nonneg _) (by + linarith only [small, delta_nonnegative]) private theorem unconditionalSmallSource_eta_scaled_root (eta : ℝ) (eta_nonnegative : 0 ≤ eta) : @@ -2040,7 +2035,7 @@ private theorem unconditionalSmallSource_root_estimates (by norm_num : (1 / 12 : ℝ) ≤ 1 / 2) have eta_bound : Real.sqrt eta ≤ R := by dsimp [R] - linarith + linarith only [alpha_root_nonnegative, eta_scaled, eta_root] have delta_root : δ ≤ alpha ^ (1 / 12 : ℝ) := by dsimp [δ] exact Real.rpow_le_rpow_of_exponent_ge' @@ -2049,10 +2044,10 @@ private theorem unconditionalSmallSource_root_estimates (by norm_num : (1 / 12 : ℝ) ≤ 1 / 3) have delta_bound : δ ≤ R := by dsimp [R] - linarith + linarith only [scaled_nonnegative, delta_root] have delta_sq_bound : δ ^ 2 ≤ R := by - linarith [mul_nonneg delta_nonnegative - (sub_nonneg.mpr delta_bounded)] + linarith only [scaled_nonnegative, delta_root, + mul_nonneg delta_nonnegative (sub_nonneg.mpr delta_bounded)] have delta_sqrt_eq : Real.sqrt δ = alpha ^ (1 / 6 : ℝ) := by dsimp [δ] rw [Real.sqrt_eq_rpow, ← Real.rpow_mul alpha_positive.le] @@ -2066,7 +2061,7 @@ private theorem unconditionalSmallSource_root_estimates (by norm_num : (0 : ℝ) ≤ 1 / 12) (by norm_num : (1 / 12 : ℝ) ≤ 1 / 6) dsimp [R] - linarith + linarith only [scaled_nonnegative, root_compare] exact ⟨root_nonnegative, eta_bound, delta_bound, delta_sq_bound, delta_sqrt_bound⟩ @@ -2093,27 +2088,19 @@ private theorem unconditionalSmallSource_clipping_sqrt_le have clip_bound : clipping ≤ 16 * eta + 12 * δ := by change clipping ≤ 16 * eta + 8 * (3 * δ / 2) at actual_clipping - linarith - have clip_base_nonnegative : 0 ≤ 16 * eta + 12 * δ := by - positivity + linarith only [actual_clipping] have clip_sqrt_base : Real.sqrt (16 * eta + 12 * δ) ≤ 4 * Real.sqrt eta + 4 * Real.sqrt δ := by - have eta_square := Real.sq_sqrt eta_nonnegative - have delta_square := Real.sq_sqrt delta_nonnegative - have clip_square := Real.sq_sqrt clip_base_nonnegative - have cross := - mul_nonneg (Real.sqrt_nonneg eta) (Real.sqrt_nonneg δ) - have clip_root_nonnegative := Real.sqrt_nonneg (16 * eta + 12 * δ) - have eta_root_nonnegative := Real.sqrt_nonneg eta - have delta_root_nonnegative := Real.sqrt_nonneg δ - nlinarith + apply (Real.sqrt_le_left (by positivity)).mpr + nlinarith only [Real.sq_sqrt eta_nonnegative, Real.sq_sqrt delta_nonnegative, + mul_nonneg (Real.sqrt_nonneg eta) (Real.sqrt_nonneg δ), delta_nonnegative] change Real.sqrt clipping ≤ 8 * R calc Real.sqrt clipping ≤ Real.sqrt (16 * eta + 12 * δ) := Real.sqrt_le_sqrt clip_bound _ ≤ 4 * Real.sqrt eta + 4 * Real.sqrt δ := clip_sqrt_base - _ ≤ 8 * R := by linarith [bounds.2.1, bounds.2.2.2.2] + _ ≤ 8 * R := by linarith only [bounds] private theorem unconditionalSmallSource_deviation_sqrt_le (eta alpha deviation : ℝ) @@ -2163,7 +2150,7 @@ private theorem unconditionalSmallSource_deviation_sqrt_le _ ≤ k * R := by apply mul_le_mul_of_nonneg_left _ k_nonnegative dsimp [R] - linarith + linarith only [scaled] theorem unconditionalSmallSourcePhysicalLoss (K eta alpha deviation clipping : ℝ) @@ -2203,9 +2190,6 @@ theorem unconditionalSmallSourcePhysicalLoss change 0 ≤ R ∧ Real.sqrt eta ≤ R ∧ δ ≤ R ∧ δ ^ 2 ≤ R ∧ Real.sqrt δ ≤ R at bounds have R_nonnegative := bounds.1 - have eta_sqrt_le_R := bounds.2.1 - have delta_le_R := bounds.2.2.1 - have delta_sq_le_R := bounds.2.2.2.1 have clip_sqrt_le := unconditionalSmallSource_clipping_sqrt_le eta alpha clipping eta_nonnegative alpha_positive alpha_bounded @@ -2219,9 +2203,6 @@ theorem unconditionalSmallSourcePhysicalLoss eta alpha deviation eta_nonnegative alpha_positive small actual_deviation change Real.sqrt deviation ≤ k * R at deviation_sqrt_le - have source_loss : - 64 * Real.sqrt eta + δ + δ ^ 2 ≤ 66 * R := by - linarith change (64 * Real.sqrt eta + δ + δ ^ 2) + 4 * Real.sqrt deviation + 4 * Real.sqrt clipping ≤ K * R @@ -2229,9 +2210,9 @@ theorem unconditionalSmallSourcePhysicalLoss (64 * Real.sqrt eta + δ + δ ^ 2) + 4 * Real.sqrt deviation + 4 * Real.sqrt clipping ≤ 66 * R + 4 * (k * R) + 4 * (8 * R) := by - linarith + linarith only [bounds, clip_sqrt_le, deviation_sqrt_le] _ ≤ (1024 + 8 * k) * R := by - linarith [mul_nonneg k_nonnegative R_nonnegative] + linarith only [bounds, mul_nonneg k_nonnegative R_nonnegative] _ ≤ K * R := by apply mul_le_mul_of_nonneg_right _ R_nonnegative simpa only [k] using lowerBound @@ -2275,7 +2256,7 @@ theorem unconditionalSmallSourcePhysicalRoundedLower have K_nonnegative : 0 ≤ K := by have root_nonnegative := Real.sqrt_nonneg (34 + unconditionalPrefactorBucketCoefficient) - linarith + linarith only [lowerBound, root_nonnegative] have R_nonnegative : 0 ≤ R := by dsimp [R] exact add_nonneg @@ -2302,7 +2283,7 @@ theorem unconditionalSmallSourcePhysicalRoundedLower (5 * lam + 2 * (K * R + Real.sqrt (8 * eta) + universalErrorCeiling K * lam)) ≤ actual - linarith + linarith only [actual_original_verifier, transfer_nonnegative, quantum_nonnegative, loss] end @@ -2320,7 +2301,7 @@ theorem pdfGreedyCeilingHorizon_le apply (div_le_iff₀ threshold).mpr have actual := mul_le_mul_of_nonneg_right small (Nat.cast_nonneg n : (0 : ℝ) ≤ n) - nlinarith + nlinarith only [actual, threshold] theorem pdfGreedyCeilingHorizon_pow_le_exp (n : ℕ) (τ d : ℝ) @@ -2332,12 +2313,12 @@ theorem pdfGreedyCeilingHorizon_pow_le_exp have base_nonnegative : 0 ≤ 1 - τ := sub_nonneg.mpr at_most_one have base_le : 1 - τ ≤ Real.exp (-τ) := by have actual := Real.add_one_le_exp (-τ) - linarith + linarith only [actual] have ceiling : d * (n : ℝ) / τ ≤ (T : ℝ) := by exact Nat.le_ceil (d * (n : ℝ) / τ) have exponent : -τ * (T : ℝ) ≤ -d * (n : ℝ) := by have cleared := (div_le_iff₀ threshold).mp ceiling - linarith + linarith only [cleared] change (1 - τ) ^ T ≤ Real.exp (-d * (n : ℝ)) calc (1 - τ) ^ T ≤ Real.exp (-τ) ^ T := by @@ -2345,7 +2326,7 @@ theorem pdfGreedyCeilingHorizon_pow_le_exp _ = Real.exp (-τ * (T : ℝ)) := by rw [← Real.exp_nat_mul] congr 1 - ring + ac_rfl _ ≤ Real.exp (-d * (n : ℝ)) := Real.exp_le_exp.mpr exponent theorem pdfGreedyCard_lt_of_ceil @@ -2394,7 +2375,7 @@ theorem pdfQuantitativeGreedyConditioning apply (div_le_iff₀ threshold).mpr have actual := mul_le_mul_of_nonneg_right rate_small (Nat.cast_nonneg n : (0 : ℝ) ≤ n) - linarith + linarith only [actual] have selected_le : D.card ≤ n := by have actual := Finset.card_le_card (Finset.subset_univ D) simpa only [ge_iff_le, card_univ, Fintype.card_fin] using actual @@ -2405,7 +2386,7 @@ theorem pdfQuantitativeGreedyConditioning have more_than_half : (n : ℝ) / 2 < ((Finset.univ \ D).card : ℝ) := by rw [remaining_real] - linarith + linarith only [strict_card, half_rate] exact ⟨D, strict_card, more_than_half, realized.trans floor, floor, positive, remaining, failure⟩ @@ -2444,8 +2425,6 @@ private theorem pdfGapRate_eq_scaled_twelfth_power (lowerBound : 0 < B) (gap : 0 < ε) (alphabet : 0 ≤ ell) : pdfGapRate B ε ell = ε / (8 * (ε + ell)) * (ε / (4 * B)) ^ 12 := by - have nonzero : B ≠ 0 := ne_of_gt lowerBound - have denominator : ε + ell ≠ 0 := ne_of_gt (by linarith) unfold pdfGapRate pdfUniversalRate field_simp @@ -2457,7 +2436,7 @@ theorem pdfGapBase_le_gap constructor · exact div_pos gap denominator · apply (div_le_iff₀ denominator).2 - nlinarith + exact le_mul_of_one_le_right gap.le (by linarith only [lowerBound]) theorem pdfGapBase_twelfth_le_gap {B ε : ℝ} @@ -2472,7 +2451,7 @@ theorem pdfGapBase_twelfth_le_gap _ ≤ ε * 1 := mul_le_mul_of_nonneg_left (pow_le_one₀ gap.le unit) gap.le - _ = ε := by ring + _ = ε := by ac_rfl theorem pdfGapBase_twelfth_le_one {B ε : ℝ} @@ -2486,10 +2465,10 @@ private theorem pdfGapRate_le_gap_div_eight (unit : ε ≤ 1) (alphabet : 0 ≤ ell) : pdfGapRate B ε ell ≤ ε / 8 := by have Bpositive : 0 < B := lt_of_lt_of_le (by norm_num) lowerBound - have denominator : 0 < ε + ell := by linarith + have denominator : 0 < ε + ell := by linarith only [gap, alphabet] have fraction : ε / (ε + ell) ≤ 1 := by apply (div_le_iff₀ denominator).2 - linarith + linarith only [alphabet] have root := pdfGapBase_twelfth_le_gap lowerBound gap unit rw [pdfGapRate_eq_scaled_twelfth_power Bpositive gap alphabet] @@ -2500,7 +2479,7 @@ private theorem pdfGapRate_le_gap_div_eight field_simp [ne_of_gt denominator, ne_of_gt Bpositive] _ ≤ 1 * ε / 8 := by gcongr - _ = ε / 8 := by ring + _ = ε / 8 := by ac_rfl private theorem pdfConditioningTolerance_bounds {ε : ℝ} (gap : 0 < ε) (unit : ε ≤ 1) : @@ -2529,9 +2508,6 @@ private theorem pdfGapRate_entropy_factor 2 * pdfGapRate B ε ell * (1 + 4 * ell / ε) = (ε / (4 * B)) ^ 12 * ((ε + 4 * ell) / (4 * (ε + ell))) := by - have nonzero : B ≠ 0 := ne_of_gt lowerBound - have gap_nonzero : ε ≠ 0 := ne_of_gt gap - have denominator : ε + ell ≠ 0 := ne_of_gt (by linarith) rw [pdfGapRate_eq_scaled_twelfth_power lowerBound gap alphabet] field_simp @@ -2559,7 +2535,7 @@ private theorem pdfGapRate_entropy_le_twelfth_power mul_le_mul_of_nonneg_left (pdfAlphabetEntropyFactor_le_one gap alphabet) nonnegative - _ = _ := by ring + _ = _ := by ac_rfl private theorem pdfCatalystAccuracy_bounds {K ε : ℝ} @@ -2570,7 +2546,7 @@ private theorem pdfCatalystAccuracy_bounds have ratio : 0 < ε / (16 * K) := div_pos gap denominator have bounded : ε / (16 * K) ≤ 1 := by apply (div_le_iff₀ denominator).2 - linarith + linarith only [lowerBound, unit] unfold pdfCatalystAccuracy exact ⟨pow_pos ratio 12, pow_le_one₀ ratio.le bounded⟩ @@ -2584,11 +2560,11 @@ theorem pdfQuantitativeEntropyRate_lt (t + (k : ℝ) * ell) / (m : ℝ) < 2 * d * (1 + ell / τ) := by have length_real : (0 : ℝ) < (n : ℝ) := by exact_mod_cast length - have mpositive : (0 : ℝ) < (m : ℝ) := by linarith + have mpositive : (0 : ℝ) < (m : ℝ) := by linarith only [remaining, length_real] have ratio_nonnegative : 0 ≤ ell / τ := div_nonneg alphabet tolerance.le have factor : 0 < d * (1 + ell / τ) := by - exact mul_pos rate (by linarith) + exact mul_pos rate (by linarith only [ratio_nonnegative]) have alphabet_bound : (k : ℝ) * ell ≤ (d * (n : ℝ) / τ) * ell := mul_le_mul_of_nonneg_right (le_of_lt conditioned) alphabet @@ -2600,9 +2576,9 @@ theorem pdfQuantitativeEntropyRate_lt add_lt_add_of_lt_of_le postselection alphabet_bound _ = d * (n : ℝ) * (1 + ell / τ) := by ring apply (div_lt_iff₀ mpositive).2 - have horizon : (n : ℝ) < 2 * (m : ℝ) := by linarith + have horizon : (n : ℝ) < 2 * (m : ℝ) := by linarith only [remaining] have scaled := mul_lt_mul_of_pos_left horizon factor - linarith + linarith only [numerator, scaled] private theorem pdfQuantitativeEntropyRate_lt_twelfth_power {B ε ell : ℝ} {n m k : ℕ} {t : ℝ} @@ -2630,7 +2606,6 @@ private theorem pdfQuantitativeEntropyRate_lt_twelfth_power (1 + ell / pdfConditioningTolerance ε) = 2 * pdfGapRate B ε ell * (1 + 4 * ell / ε) := by unfold pdfConditioningTolerance - have nonzero : ε ≠ 0 := ne_of_gt gap field_simp rw [rewrite] at entropy exact lt_of_lt_of_le entropy @@ -2675,7 +2650,7 @@ theorem pdfEntropyRoundingLoss_lt_gapQuarter (entropy : 0 ≤ η) (small : η < (ε / (4 * B)) ^ (12 : ℕ)) : B * η ^ (1 / 12 : ℝ) < ε / 4 := by - have coefficient : 0 < B := by linarith + have coefficient : 0 < B := by linarith only [lowerBound] calc B * η ^ (1 / 12 : ℝ) < B * (ε / (4 * B)) := mul_lt_mul_of_pos_left @@ -2688,7 +2663,6 @@ private theorem pdfCatalystAccuracy_samplingLoss {K ε : ℝ} (lowerBound : 1 ≤ K) (gap : 0 < ε) : 2 * K * (pdfCatalystAccuracy K ε) ^ (1 / 12 : ℝ) = ε / 8 := by - have coefficient : 0 < K := by linarith rw [pdfCatalystAccuracy_twelfth_root lowerBound gap] field_simp norm_num @@ -2708,7 +2682,6 @@ private def pdfRoundingCoefficient (K : ℝ) : ℝ := theorem pdfUniversalErrorCeiling_pos {K : ℝ} (lowerBound : 1 ≤ K) : 0 < universalErrorCeiling K := by - have nonnegative : 0 ≤ K := by linarith unfold universalErrorCeiling positivity @@ -2726,7 +2699,7 @@ private theorem pdfRoundingCoefficient_two_le have eight : 1 ≤ Real.sqrt (8 : ℝ) := Real.one_le_sqrt.mpr (by norm_num) unfold pdfRoundingCoefficient - linarith + linarith only [first_nonnegative, quantum_nonnegative, eight] private theorem pdfRoundingCoefficient_one_le {K : ℝ} (lowerBound : 1 ≤ K) : @@ -2788,7 +2761,7 @@ private theorem pdfQuantitativeRoundingLoss positivity have classical_coefficient : 0 ≤ 5 + 2 * universalErrorCeiling K := by - linarith + linarith only [ceiling] have pinsker_bound := pdfPinskerRoot_le_twelfthRoot nonnegative bounded pinsker have weighted_pinsker : @@ -2802,7 +2775,6 @@ private theorem pdfQuantitativeRoundingLoss 2 * Real.sqrt (8 * eta) ≤ 2 * (Real.sqrt (8 : ℝ) * eta ^ (1 / 12 : ℝ)) := mul_le_mul_of_nonneg_left sqrt_bound (by norm_num) - have source_bounds := add_le_add weighted_pinsker weighted_sqrt calc totalSamplingLoss K alpha eta (kappa + gamma) = 2 * K * alpha ^ (1 / 12 : ℝ) + @@ -2943,7 +2915,10 @@ private theorem pdfConstantStrategy_outcomeProbability ((if a' = a then (1 : Matrix PUnit PUnit ℂ) else 0) ⊗ₖ (if b' = b then (1 : Matrix PUnit PUnit ℂ) else 0)))).re = _ by_cases alice : a' = a <;> by_cases bob : b' = b <;> - simp [alice, bob, Matrix.trace_one] + simp only [alice, ↓reduceIte, bob, zero_mul, implies_true, mul_zero, mul_one, + kroneckerMap_one_one, trace_one, Fintype.card_prod, Fintype.card_unique, Nat.cast_one, + one_re, and_self, kroneckerMap_zero_right, trace_zero, zero_re, and_false, + kroneckerMap_zero_left, and_true] private theorem pdfConstantStrategy_winProbability (G : Game X Y A B) (a : A) (b : B) : @@ -2985,7 +2960,7 @@ private theorem pdfQuestionWeight_le_constantStrategy exact Finset.single_le_sum (f := fun y' : Y => if G.predicate x y' a b = true then G.questionWeight x y' else 0) - (fun y' _ => by split_ifs <;> simp [G.weight_nonneg]) + (fun y' _ => by split_ifs <;> simp only [G.weight_nonneg, Std.le_refl]) (Finset.mem_univ y) _ ≤ ∑ x' : X, ∑ y' : Y, if G.predicate x' y' a b = true then G.questionWeight x' y' else 0 := by @@ -2993,7 +2968,7 @@ private theorem pdfQuestionWeight_le_constantStrategy (f := fun x' : X => ∑ y' : Y, if G.predicate x' y' a b = true then G.questionWeight x' y' else 0) (fun x' _ => Finset.sum_nonneg - (fun y' _ => by split_ifs <;> simp [G.weight_nonneg])) + (fun y' _ => by split_ifs <;> simp only [G.weight_nonneg, Std.le_refl])) (Finset.mem_univ x) theorem pdfPredicate_not_accepted_of_entangledValue_eq_zero @@ -3011,7 +2986,7 @@ theorem pdfPredicate_not_accepted_of_entangledValue_eq_zero unfold entangledValue exact le_csSup (winProbabilities_bddAbove G) ⟨pdfConstantStrategy G a b, rfl⟩ - linarith + linarith only [zero, supported, lower, upper] theorem pdfRepeatedEntangledValue_eq_zero_of_entangledValue_eq_zero (G : Game X Y A B) @@ -3064,8 +3039,8 @@ theorem pdfAlphabetEntropy_nonneg have bob_real : (1 : ℝ) ≤ (Fintype.card B : ℝ) := by exact_mod_cast bob_card apply Real.log_nonneg - linarith [mul_nonneg (sub_nonneg.mpr alice_real) - (sub_nonneg.mpr bob_real)] + linarith only [alice_real, bob_real, + mul_nonneg (sub_nonneg.mpr alice_real) (sub_nonneg.mpr bob_real)] theorem pdfGap_le_one {X Y A B : Type} @@ -3088,7 +3063,7 @@ theorem pdfPostselectionLogCost_lt_of_exponential rw [Real.log_exp] at logarithm unfold postselectionLogCost rw [one_div, Real.log_inv] - linarith + linarith only [logarithm] theorem pdfPinskerRate_le_sqrt_martingaleRate {X Y A B : Type} @@ -3159,7 +3134,7 @@ private theorem pdfFullQuantitativeSamplingLoss (K := K) (alpha := pdfCatalystAccuracy K ε) (eta := eta) (kappa := kappa) (gamma := ε / (16 * (5 + 2 * universalErrorCeiling K))) - (by linarith) entropy bounded pinsker + (by linarith only [lowerBound]) entropy bounded pinsker have entropy_loss : pdfRoundingCoefficient K * eta ^ (1 / 12 : ℝ) < ε / 4 := @@ -3177,7 +3152,7 @@ private theorem pdfFullQuantitativeSamplingLoss (ε / (16 * (5 + 2 * universalErrorCeiling K))) = ε / 16 := by field_simp - linarith + linarith only [gap, loss, entropy_loss, catalyst_loss, gamma_loss] theorem pdf_distributionUniformExponential_of_uniform_source_rounding (rounding : @@ -3242,9 +3217,9 @@ theorem pdf_distributionUniformExponential_of_uniform_source_rounding have tolerance_lt_one : τ < 1 := by have at_most := tolerance.2 dsimp [τ] - linarith + linarith only [tolerance] have rate_positive : 0 < d := - pdfGapRate_pos (by linarith) gap alphabet + pdfGapRate_pos (by linarith only [coefficient, tolerance]) gap alphabet have rate_small : d ≤ τ / 2 := pdfGapRate_le_half_conditioningTolerance coefficient gap unit alphabet @@ -3305,7 +3280,7 @@ theorem pdf_distributionUniformExponential_of_uniform_source_rounding (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < ε / 4 := by simpa [τ, pdfConditioningTolerance] using failure - linarith + linarith only [game_gap, actual] obtain ⟨rounded, rounded_bound⟩ := round G n S D remaining positive alpha gamma alpha_positive alpha_at_most_one gamma_positive source_failure @@ -3491,8 +3466,6 @@ theorem unconditionalSourcePhysicalRounding_exists_fairStoppingHazard let delta : ℝ := alpha ^ (1 / 3 : ℝ) let t : ℝ := Real.sqrt (64 * Real.sqrt eta + delta) let rho : ℝ := alpha ^ (1 / 12 : ℝ) - have eta_nonnegative : 0 ≤ eta := - martingaleRate_nonneg G n S D remaining positive have delta_positive : 0 < delta := Real.rpow_pos_of_pos alpha_positive _ have delta_bounded : delta ≤ 1 := @@ -3500,14 +3473,10 @@ theorem unconditionalSourcePhysicalRounding_exists_fairStoppingHazard have t_positive : 0 < t := by dsimp [t] apply Real.sqrt_pos.2 - linarith [Real.sqrt_nonneg eta] + linarith only [delta_positive, Real.sqrt_nonneg eta] have t_bounded : t ≤ 1 := by - dsimp [t] - have bound : 64 * Real.sqrt eta + delta ≤ 1 := by - simpa [eta, delta] using small - nlinarith [Real.sqrt_nonneg - (64 * Real.sqrt eta + delta), - Real.sq_sqrt (show 0 ≤ 64 * Real.sqrt eta + delta by positivity)] + dsimp only [t] + exact Real.sqrt_le_one.mpr small have rho_positive : 0 < rho := Real.rpow_pos_of_pos alpha_positive _ obtain ⟨w, N, width_large, grid, budget, scalar, canonical, _⟩ := @@ -3580,17 +3549,15 @@ theorem unconditionalSourcePhysicalRounding_largeVerifierBound Real.rpow_nonneg eta_nonnegative _ have alpha_root_nonnegative : 0 ≤ alpha ^ (1 / 12 : ℝ) := Real.rpow_nonneg alpha_positive.le _ - have scaled_nonnegative : 0 ≤ (32 * eta) ^ (1 / 12 : ℝ) := - Real.rpow_nonneg (by positivity) _ have root_scaled : eta ^ (1 / 12 : ℝ) ≤ (32 * eta) ^ (1 / 12 : ℝ) := by apply Real.rpow_le_rpow eta_nonnegative - · linarith + · linarith only [eta_nonnegative] · norm_num have root_sum_nonnegative : 0 ≤ eta ^ (1 / 12 : ℝ) + alpha ^ (1 / 12 : ℝ) := add_nonneg eta_root_nonnegative alpha_root_nonnegative - have constant_nonnegative : 0 ≤ K := by linarith + have constant_nonnegative : 0 ≤ K := by linarith only [lowerBound] have universal_nonnegative : 0 ≤ universalErrorCeiling K := by unfold universalErrorCeiling positivity @@ -3607,7 +3574,7 @@ theorem unconditionalSourcePhysicalRounding_largeVerifierBound _ ≤ K * (alpha ^ (1 / 12 : ℝ) + (32 * eta) ^ (1 / 12 : ℝ)) := by apply mul_le_mul lowerBound - · linarith + · linarith only [root_scaled] · exact root_sum_nonnegative · exact constant_nonnegative have lam_error : 0 ≤ universalErrorCeiling K * lam := @@ -3615,7 +3582,7 @@ theorem unconditionalSourcePhysicalRounding_largeVerifierBound have sqrt_error : 0 ≤ Real.sqrt (8 * eta) := Real.sqrt_nonneg _ unfold roundedWinningLowerBound totalSamplingLoss - linarith + linarith only [lam_nonnegative, epsilon_nonnegative, quantum, lam_error, sqrt_error] theorem unconditionalSourcePhysicalRounding_exists_large {X Y A B : Type} @@ -3647,7 +3614,7 @@ theorem unconditionalSourcePhysicalRounding_exists_large have eta_nonnegative := martingaleRate_nonneg G n S D remaining positive have epsilon_nonnegative : 0 ≤ 1 - entangledValue G := by - linarith [entangledValue_le_one G] + linarith only [entangledValue_le_one G] have pinsker_nonnegative : 0 ≤ exactSourcePinskerRate G n S D := by unfold exactSourcePinskerRate @@ -3658,7 +3625,7 @@ theorem unconditionalSourcePhysicalRounding_exists_large (exactSourcePinskerRate G n S D + gamma) (1 - entangledValue G) lowerBound eta_nonnegative alpha_positive alpha_bounded - (by linarith) epsilon_nonnegative large + (by linarith only [gamma_positive, pinsker_nonnegative]) epsilon_nonnegative large exact source_bound.trans rounded.winProbability_nonneg theorem unconditionalSourcePhysicalRounding_smallRoundedLower @@ -3724,7 +3691,7 @@ theorem unconditionalSourcePhysicalRounding_smallRoundedLower 0 ≤ exactSourcePinskerRate G n S D := by unfold exactSourcePinskerRate positivity - linarith + linarith only [gamma_positive, pinsker_nonnegative] · exact actual_original_verifier theorem @@ -3776,7 +3743,7 @@ theorem G n S D remaining positive alpha gamma deviation clipping alpha_positive alpha_bounded gamma_positive small actual_deviation actual_clipping rounded - linarith [Real.sqrt_nonneg clipping, + linarith only [stopped_verifier, Real.sqrt_nonneg clipping, Real.sqrt_nonneg (8 * martingaleRate G n S D)] theorem unconditionalSourceOneGameRounding_uniform_of_small