From ffa4a9682119e39c0bd6f14e1e0b2b06baed0ab7 Mon Sep 17 00:00:00 2001 From: Harald Husum Date: Sun, 21 Dec 2025 22:13:30 +0100 Subject: [PATCH] chore(Computability): fix whitespace --- .../Computability/AkraBazzi/AkraBazzi.lean | 8 ++--- .../AkraBazzi/GrowsPolynomially.lean | 34 +++++++++---------- Mathlib/Computability/NFA.lean | 2 +- Mathlib/Computability/TMToPartrec.lean | 2 +- 4 files changed, 23 insertions(+), 23 deletions(-) diff --git a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean index a02b23009c5d0f..a11221fa82e238 100644 --- a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean +++ b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean @@ -188,7 +188,7 @@ lemma growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn (p : ℝ) : (GrowsPolynomially.pow 2 growsPolynomially_log ?_) filter_upwards [eventually_ge_atTop 1] with _ hx using log_nonneg hx | inr hp => -- p ≠ 0 - refine GrowsPolynomially.of_isTheta (growsPolynomially_rpow (p-1)) + refine GrowsPolynomially.of_isTheta (growsPolynomially_rpow (p - 1)) (isTheta_deriv_rpow_p_mul_one_sub_smoothingFn hp) ?_ filter_upwards [eventually_gt_atTop 0] with _ _ positivity @@ -208,7 +208,7 @@ lemma growsPolynomially_deriv_rpow_p_mul_one_add_smoothingFn (p : ℝ) : (GrowsPolynomially.pow 2 growsPolynomially_log ?_) filter_upwards [eventually_ge_atTop 1] with x hx using log_nonneg hx | inr hp => -- p ≠ 0 - refine GrowsPolynomially.of_isTheta (growsPolynomially_rpow (p-1)) + refine GrowsPolynomially.of_isTheta (growsPolynomially_rpow (p - 1)) (isTheta_deriv_rpow_p_mul_one_add_smoothingFn hp) ?_ filter_upwards [eventually_gt_atTop 0] with _ _ positivity @@ -583,9 +583,9 @@ lemma T_isBigO_smoothingFn_mul_asympBound : refine mul_nonpos_of_nonpos_of_nonneg ?_ g_pos rw [sub_nonpos] calc 1 - _ ≤ 2 * (c₁⁻¹ * c₁) * (1/2) := by + _ ≤ 2 * (c₁⁻¹ * c₁) * (1 / 2) := by rw [inv_mul_cancel₀ (by positivity : c₁ ≠ 0)]; norm_num - _ = (2 * c₁⁻¹) * c₁ * (1/2) := by ring + _ = (2 * c₁⁻¹) * c₁ * (1 / 2) := by ring _ ≤ C * c₁ * (1 - ε n) := by gcongr · rw [hC]; exact le_max_left _ _ diff --git a/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean b/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean index 9e86e22b99fccf..a94c527389ceb1 100644 --- a/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean +++ b/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean @@ -220,7 +220,7 @@ lemma eventually_atTop_nonneg_or_nonpos (hf : GrowsPolynomially f) : _ ≤ ((1 : ℝ) / (2 : ℝ)) * (2 : ℝ) ^ n * max n₀ 2 := by gcongr; norm_num _ ≤ _ := by rw [mul_assoc]; gcongr; exact_mod_cast hz.1 case ub => - have h₁ : (2 : ℝ)^n = ((1 : ℝ)/(2 : ℝ)) * (2 : ℝ)^(n + 1) := by + have h₁ : (2 : ℝ)^n = ((1 : ℝ) / (2 : ℝ)) * (2 : ℝ)^(n + 1) := by rw [one_div, pow_add, pow_one] ring rw [h₁, mul_assoc] @@ -417,10 +417,10 @@ lemma GrowsPolynomially.add_isLittleO {f g : ℝ → ℝ} (hf : GrowsPolynomiall have hfg₂ : ‖g x‖ ≤ 1 / 2 * f x := by calc ‖g x‖ ≤ 1 / 2 * ‖f x‖ := hfg' x hbx _ = 1 / 2 * f x := by congr; exact norm_of_nonneg (hf₂ _ hbx) - have hx_ub : f x + g x ≤ 3/2 * f x := by + have hx_ub : f x + g x ≤ 3 / 2 * f x := by calc _ ≤ f x + ‖g x‖ := by gcongr; exact le_norm_self (g x) _ ≤ f x + 1 / 2 * f x := by gcongr - _ = 3/2 * f x := by ring + _ = 3 / 2 * f x := by ring have hx_lb : 1 / 2 * f x ≤ f x + g x := by calc f x + g x ≥ f x - ‖g x‖ := by rw [sub_eq_add_neg, norm_eq_abs]; gcongr; exact neg_abs_le (g x) @@ -438,15 +438,15 @@ lemma GrowsPolynomially.add_isLittleO {f g : ℝ → ℝ} (hf : GrowsPolynomiall _ ≥ f u - 1 / 2 * f u := by gcongr _ = 1 / 2 * f u := by ring _ ≥ 1 / 2 * (c₁ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).1 - _ = c₁/3 * (3/2 * f x) := by ring - _ ≥ c₁/3 * (f x + g x) := by gcongr + _ = c₁ / 3 * (3 / 2 * f x) := by ring + _ ≥ c₁ / 3 * (f x + g x) := by gcongr case ub => calc _ ≤ f u + ‖g u‖ := by gcongr; exact le_norm_self (g u) _ ≤ f u + 1 / 2 * f u := by gcongr - _ = 3/2 * f u := by ring - _ ≤ 3/2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2 - _ = 3*c₂ * (1 / 2 * f x) := by ring - _ ≤ 3*c₂ * (f x + g x) := by gcongr + _ = 3 / 2 * f u := by ring + _ ≤ 3 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2 + _ = 3 * c₂ * (1 / 2 * f x) := by ring + _ ≤ 3 * c₂ * (f x + g x) := by gcongr | inr hf' => -- f is eventually nonpos have hf := hf b hb obtain ⟨c₁, hc₁_mem : 0 < c₁, c₂, hc₂_mem : 0 < c₂, hf⟩ := hf @@ -465,7 +465,7 @@ lemma GrowsPolynomially.add_isLittleO {f g : ℝ → ℝ} (hf : GrowsPolynomiall calc _ ≤ f x + ‖g x‖ := by gcongr; exact le_norm_self (g x) _ ≤ f x + (-1 / 2 * f x) := by gcongr _ = 1 / 2 * f x := by ring - have hx_lb : 3/2 * f x ≤ f x + g x := by + have hx_lb : 3 / 2 * f x ≤ f x + g x := by calc f x + g x ≥ f x - ‖g x‖ := by rw [sub_eq_add_neg, norm_eq_abs]; gcongr; exact neg_abs_le (g x) _ ≥ f x + 1 / 2 * f x := by @@ -473,7 +473,7 @@ lemma GrowsPolynomially.add_isLittleO {f g : ℝ → ℝ} (hf : GrowsPolynomiall gcongr refine le_of_neg_le_neg ?bc.a rwa [neg_neg, ← neg_mul, ← neg_div] - _ = 3/2 * f x := by ring + _ = 3 / 2 * f x := by ring intro u ⟨hu_lb, hu_ub⟩ have hfu_nonpos : f u ≤ 0 := hf₂ _ hu_lb have hfg₃ : ‖g u‖ ≤ -1 / 2 * f u := by @@ -489,10 +489,10 @@ lemma GrowsPolynomially.add_isLittleO {f g : ℝ → ℝ} (hf : GrowsPolynomiall gcongr refine le_of_neg_le_neg ?_ rwa [neg_neg, ← neg_mul, ← neg_div] - _ = 3/2 * f u := by ring - _ ≥ 3/2 * (c₁ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).1 - _ = 3*c₁ * (1 / 2 * f x) := by ring - _ ≥ 3*c₁ * (f x + g x) := by gcongr + _ = 3 / 2 * f u := by ring + _ ≥ 3 / 2 * (c₁ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).1 + _ = 3 * c₁ * (1 / 2 * f x) := by ring + _ ≥ 3 * c₁ * (f x + g x) := by gcongr case ub => calc _ ≤ f u + ‖g u‖ := by gcongr; exact le_norm_self (g u) _ ≤ f u - 1 / 2 * f u := by @@ -501,8 +501,8 @@ lemma GrowsPolynomially.add_isLittleO {f g : ℝ → ℝ} (hf : GrowsPolynomiall rwa [← neg_mul, ← neg_div] _ = 1 / 2 * f u := by ring _ ≤ 1 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2 - _ = c₂/3 * (3/2 * f x) := by ring - _ ≤ c₂/3 * (f x + g x) := by gcongr + _ = c₂ / 3 * (3 / 2 * f x) := by ring + _ ≤ c₂ / 3 * (f x + g x) := by gcongr protected lemma GrowsPolynomially.inv {f : ℝ → ℝ} (hf : GrowsPolynomially f) : GrowsPolynomially fun x => (f x)⁻¹ := by diff --git a/Mathlib/Computability/NFA.lean b/Mathlib/Computability/NFA.lean index 321b5c9c9c176b..15026d9b508da6 100644 --- a/Mathlib/Computability/NFA.lean +++ b/Mathlib/Computability/NFA.lean @@ -138,7 +138,7 @@ theorem evalFrom_iUnion {ι : Sort*} (s : ι → Set σ) (x : List α) : M.evalFrom (⋃ i, s i) x = ⋃ i, M.evalFrom (s i) x := by induction x generalizing s with | nil => simp - | cons a x ih => simp [stepSet, Set.iUnion_comm (ι:=σ) (ι':=ι), ih] + | cons a x ih => simp [stepSet, Set.iUnion_comm (ι := σ) (ι' := ι), ih] variable (M) in theorem evalFrom_iUnion₂ {ι : Sort*} {κ : ι → Sort*} (f : ∀ i, κ i → Set σ) (x : List α) : diff --git a/Mathlib/Computability/TMToPartrec.lean b/Mathlib/Computability/TMToPartrec.lean index 0e5e094c0ab5a2..2b259d1fee7b2a 100644 --- a/Mathlib/Computability/TMToPartrec.lean +++ b/Mathlib/Computability/TMToPartrec.lean @@ -972,7 +972,7 @@ theorem trStmts₁_trans {q q'} : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trSt · exact Or.inr (Or.inr <| Or.inr <| q₂_ih h h') theorem trStmts₁_self (q) : q ∈ trStmts₁ q := by - induction q <;> · first | apply Finset.mem_singleton_self|apply Finset.mem_insert_self + induction q <;> · first | apply Finset.mem_singleton_self | apply Finset.mem_insert_self /-- The (finite!) set of machine states visited during the course of evaluation of `c`, including the state `ret k` but not any states after that (that is, the states visited while