ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type w<VAR>C : Type uC<VAR>inst✝³ : Category.{uC', uC} C<VAR>inst✝² : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝¹ : Category.{uD', uD} D<VAR>inst✝ : HasZeroMorphisms D<VAR>F f : J → C<VAR>t : Bicone f<VAR>ht : IsLimit t.toCone<VAR>j : J<VAR>j' : Discrete J<GOAL>t.ι j ≫ t.toCone.π.app j' = (Fan.mk (f j) fun j' => if h : j = j' then eqToHom ⋯ else 0).π.app j'
<VAR>b x✝ y x : ℝ<GOAL>logb b |x| = logb b x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>b' : ℝ := b (min_bi b) / 2<GOAL>T =O[atTop] fun n => (1 - ε ↑n) * asympBound g a b n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<GOAL>T =O[atTop] fun n => (1 - ε ↑n) * asympBound g a b n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<GOAL>∀ᶠ (n₀ : ℕ) in atTop, ∃ c, ∀ n ≥ n₀, ‖T n‖ ≤ c * ‖(1 - ε ↑n) * asympBound g a b n‖
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<VAR>c₁ : ℝ<VAR>hc₁ : c₁ > 0<VAR>h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n<GOAL>∀ᶠ (n₀ : ℕ) in atTop, ∃ c, ∀ n ≥ n₀, ‖T n‖ ≤ c * ‖(1 - ε ↑n) * asympBound g a b n‖
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<VAR>c₁ : ℝ<VAR>hc₁ : c₁ > 0<VAR>h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n<VAR>n₀ : ℕ<VAR>n₀_ge_Rn₀ : R.n₀ ≤ n₀<VAR>h_smoothing_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < 1 - ε ↑y<VAR>h_smoothing_gt_half : ∀ (y : ℕ), n₀ ≤ y → 1 / 2 < 1 - ε ↑y<VAR>h_asympBound_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < asympBound g a b y<VAR>h_asympBound_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < asympBound g a b (r i y)<VAR>h_asympBound_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < asympBound g a b y<VAR>n₀_pos : 0 < n₀<VAR>h_smoothing_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < 1 - ε ↑(r i y)<VAR>bound1 : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), ↑(r i y) ^ p a b * (1 - ε ↑(r i y)) ≤ b i ^ p a b * ↑y ^ p a b * (1 - ε ↑y)<VAR>h_smoothingFn_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 - ε ↑y<VAR>h_sumTransform : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), c₁ * g ↑y ≤ sumTransform (p a b) g (r i y) y<VAR>h_bi_le_r : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b (min_bi b) / 2 * ↑y ≤ ↑(r i y)<GOAL>∃ c, ∀ n ≥ n₀, ‖T n‖ ≤ c * ‖(1 - ε ↑n) * asympBound g a b n‖
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<VAR>c₁ : ℝ<VAR>hc₁ : c₁ > 0<VAR>h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n<VAR>n₀ : ℕ<VAR>n₀_ge_Rn₀ : R.n₀ ≤ n₀<VAR>h_smoothing_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < 1 - ε ↑y<VAR>h_smoothing_gt_half : ∀ (y : ℕ), n₀ ≤ y → 1 / 2 < 1 - ε ↑y<VAR>h_asympBound_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < asympBound g a b y<VAR>h_asympBound_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < asympBound g a b (r i y)<VAR>h_asympBound_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < asympBound g a b y<VAR>n₀_pos : 0 < n₀<VAR>h_smoothing_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < 1 - ε ↑(r i y)<VAR>bound1 : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), ↑(r i y) ^ p a b * (1 - ε ↑(r i y)) ≤ b i ^ p a b * ↑y ^ p a b * (1 - ε ↑y)<VAR>h_smoothingFn_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 - ε ↑y<VAR>h_sumTransform : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), c₁ * g ↑y ≤ sumTransform (p a b) g (r i y) y<VAR>h_bi_le_r : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b (min_bi b) / 2 * ↑y ≤ ↑(r i y)<VAR>h_base_nonempty : (Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀).Nonempty<GOAL>∃ c, ∀ n ≥ n₀, ‖T n‖ ≤ c * ‖(1 - ε ↑n) * asympBound g a b n‖
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<VAR>c₁ : ℝ<VAR>hc₁ : c₁ > 0<VAR>h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n<VAR>n₀ : ℕ<VAR>n₀_ge_Rn₀ : R.n₀ ≤ n₀<VAR>h_smoothing_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < 1 - ε ↑y<VAR>h_smoothing_gt_half : ∀ (y : ℕ), n₀ ≤ y → 1 / 2 < 1 - ε ↑y<VAR>h_asympBound_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < asympBound g a b y<VAR>h_asympBound_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < asympBound g a b (r i y)<VAR>h_asympBound_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < asympBound g a b y<VAR>n₀_pos : 0 < n₀<VAR>h_smoothing_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < 1 - ε ↑(r i y)<VAR>bound1 : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), ↑(r i y) ^ p a b * (1 - ε ↑(r i y)) ≤ b i ^ p a b * ↑y ^ p a b * (1 - ε ↑y)<VAR>h_smoothingFn_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 - ε ↑y<VAR>h_sumTransform : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), c₁ * g ↑y ≤ sumTransform (p a b) g (r i y) y<VAR>h_bi_le_r : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b (min_bi b) / 2 * ↑y ≤ ↑(r i y)<VAR>h_base_nonempty : (Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀).Nonempty<VAR>base_max : ℝ := (Ico ⌊b' * ↑n₀⌋₊ n₀).sup' h_base_nonempty fun n => T n / ((1 - ε ↑n) * asympBound g a b n)<VAR>C : ℝ := max (2 * c₁⁻¹) base_max<VAR>hC : C = max (2 * c₁⁻¹) base_max<VAR>n : ℕ<VAR>hn : n ≥ n₀<GOAL>‖T n‖ ≤ C * ‖(1 - ε ↑n) * asympBound g a b n‖
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<VAR>c₁ : ℝ<VAR>hc₁ : c₁ > 0<VAR>h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n<VAR>n₀ : ℕ<VAR>n₀_ge_Rn₀ : R.n₀ ≤ n₀<VAR>h_smoothing_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < 1 - ε ↑y<VAR>h_smoothing_gt_half : ∀ (y : ℕ), n₀ ≤ y → 1 / 2 < 1 - ε ↑y<VAR>h_asympBound_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < asympBound g a b y<VAR>h_asympBound_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < asympBound g a b (r i y)<VAR>h_asympBound_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < asympBound g a b y<VAR>n₀_pos : 0 < n₀<VAR>h_smoothing_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < 1 - ε ↑(r i y)<VAR>bound1 : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), ↑(r i y) ^ p a b * (1 - ε ↑(r i y)) ≤ b i ^ p a b * ↑y ^ p a b * (1 - ε ↑y)<VAR>h_smoothingFn_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 - ε ↑y<VAR>h_sumTransform : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), c₁ * g ↑y ≤ sumTransform (p a b) g (r i y) y<VAR>h_bi_le_r : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b (min_bi b) / 2 * ↑y ≤ ↑(r i y)<VAR>h_base_nonempty : (Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀).Nonempty<VAR>base_max : ℝ := (Ico ⌊b' * ↑n₀⌋₊ n₀).sup' h_base_nonempty fun n => T n / ((1 - ε ↑n) * asympBound g a b n)<VAR>C : ℝ := max (2 * c₁⁻¹) base_max<VAR>hC : C = max (2 * c₁⁻¹) base_max<VAR>n : ℕ<VAR>hn : n ≥ n₀<VAR>h_base : ∀ n ∈ Ico ⌊b' * ↑n₀⌋₊ n₀, T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)<GOAL>‖T n‖ ≤ C * ‖(1 - ε ↑n) * asympBound g a b n‖
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<VAR>c₁ : ℝ<VAR>hc₁ : c₁ > 0<VAR>h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n<VAR>n₀ : ℕ<VAR>n₀_ge_Rn₀ : R.n₀ ≤ n₀<VAR>h_smoothing_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < 1 - ε ↑y<VAR>h_smoothing_gt_half : ∀ (y : ℕ), n₀ ≤ y → 1 / 2 < 1 - ε ↑y<VAR>h_asympBound_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < asympBound g a b y<VAR>h_asympBound_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < asympBound g a b (r i y)<VAR>h_asympBound_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < asympBound g a b y<VAR>n₀_pos : 0 < n₀<VAR>h_smoothing_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < 1 - ε ↑(r i y)<VAR>bound1 : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), ↑(r i y) ^ p a b * (1 - ε ↑(r i y)) ≤ b i ^ p a b * ↑y ^ p a b * (1 - ε ↑y)<VAR>h_smoothingFn_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 - ε ↑y<VAR>h_sumTransform : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), c₁ * g ↑y ≤ sumTransform (p a b) g (r i y) y<VAR>h_bi_le_r : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b (min_bi b) / 2 * ↑y ≤ ↑(r i y)<VAR>h_base_nonempty : (Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀).Nonempty<VAR>base_max : ℝ := (Ico ⌊b' * ↑n₀⌋₊ n₀).sup' h_base_nonempty fun n => T n / ((1 - ε ↑n) * asympBound g a b n)<VAR>C : ℝ := max (2 * c₁⁻¹) base_max<VAR>hC : C = max (2 * c₁⁻¹) base_max<VAR>n : ℕ<VAR>hn : n ≥ n₀<VAR>h_base : ∀ n ∈ Ico ⌊b' * ↑n₀⌋₊ n₀, T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)<VAR>h_asympBound_pos' : 0 < asympBound g a b n<VAR>h_one_sub_smoothingFn_pos' : 0 < 1 - ε ↑n<GOAL>‖T n‖ ≤ C * ‖(1 - ε ↑n) * asympBound g a b n‖
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>b' : ℝ := b (min_bi b) / 2<VAR>hb_pos : 0 < b'<VAR>c₁ : ℝ<VAR>hc₁ : c₁ > 0<VAR>h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n<VAR>n₀ : ℕ<VAR>n₀_ge_Rn₀ : R.n₀ ≤ n₀<VAR>h_smoothing_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < 1 - ε ↑y<VAR>h_smoothing_gt_half : ∀ (y : ℕ), n₀ ≤ y → 1 / 2 < 1 - ε ↑y<VAR>h_asympBound_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < asympBound g a b y<VAR>h_asympBound_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < asympBound g a b (r i y)<VAR>h_asympBound_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < asympBound g a b y<VAR>n₀_pos : 0 < n₀<VAR>h_smoothing_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < 1 - ε ↑(r i y)<VAR>bound1 : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), ↑(r i y) ^ p a b * (1 - ε ↑(r i y)) ≤ b i ^ p a b * ↑y ^ p a b * (1 - ε ↑y)<VAR>h_smoothingFn_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 - ε ↑y<VAR>h_sumTransform : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), c₁ * g ↑y ≤ sumTransform (p a b) g (r i y) y<VAR>h_bi_le_r : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b (min_bi b) / 2 * ↑y ≤ ↑(r i y)<VAR>h_base_nonempty : (Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀).Nonempty<VAR>base_max : ℝ := (Ico ⌊b' * ↑n₀⌋₊ n₀).sup' h_base_nonempty fun n => T n / ((1 - ε ↑n) * asympBound g a b n)<VAR>C : ℝ := max (2 * c₁⁻¹) base_max<VAR>hC : C = max (2 * c₁⁻¹) base_max<VAR>n : ℕ<VAR>hn : n ≥ n₀<VAR>h_base : ∀ n ∈ Ico ⌊b' * ↑n₀⌋₊ n₀, T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)<VAR>h_asympBound_pos' : 0 < asympBound g a b n<VAR>h_one_sub_smoothingFn_pos' : 0 < 1 - ε ↑n<GOAL>T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : StrictConvexSpace ℝ F<VAR>f : E → ℂ<VAR>c : E<VAR>hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z<VAR>hc : IsLocalMin (norm ∘ f) c<GOAL>(∀ᶠ (z : E) in 𝓝 c, f z = f c) ∨ f c = 0
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : StrictConvexSpace ℝ F<VAR>f : E → ℂ<VAR>c : E<VAR>hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z<VAR>hc : IsLocalMin (norm ∘ f) c<VAR>h : ¬f c = 0<GOAL>∀ᶠ (z : E) in 𝓝 c, f z = f c
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : StrictConvexSpace ℝ F<VAR>f : E → ℂ<VAR>c : E<VAR>hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z<VAR>hc : IsLocalMin (norm ∘ f) c<VAR>h : ¬f c = 0<VAR>h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0<GOAL>∀ᶠ (z : E) in 𝓝 c, f z = f c
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : StrictConvexSpace ℝ F<VAR>f : E → ℂ<VAR>c : E<VAR>hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z<VAR>hc : IsLocalMin (norm ∘ f) c<VAR>h : ¬f c = 0<VAR>h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0<VAR>h2 : IsLocalMax (norm ∘ f)⁻¹ c<GOAL>∀ᶠ (z : E) in 𝓝 c, f z = f c
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : StrictConvexSpace ℝ F<VAR>f : E → ℂ<VAR>c : E<VAR>hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z<VAR>hc : IsLocalMin (norm ∘ f) c<VAR>h : ¬f c = 0<VAR>h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0<VAR>h2 : IsLocalMax (norm ∘ f)⁻¹ c<VAR>h3 : IsLocalMax (norm ∘ f⁻¹) c<GOAL>∀ᶠ (z : E) in 𝓝 c, f z = f c
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : StrictConvexSpace ℝ F<VAR>f : E → ℂ<VAR>c : E<VAR>hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z<VAR>hc : IsLocalMin (norm ∘ f) c<VAR>h : ¬f c = 0<VAR>h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0<VAR>h2 : IsLocalMax (norm ∘ f)⁻¹ c<VAR>h3 : IsLocalMax (norm ∘ f⁻¹) c<VAR>h4 : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f⁻¹ z<GOAL>∀ᶠ (z : E) in 𝓝 c, f z = f c
<VAR>K : Type u_1<VAR>n : ℕ<VAR>g : GenContFract K<VAR>s : Stream'.Seq (Pair K)<VAR>inst✝ : Field K<VAR>nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0<GOAL>g.convs (n + 1) = (g.squashGCF n).convs n
<VAR>K : Type u_1<VAR>n : ℕ<VAR>g : GenContFract K<VAR>s : Stream'.Seq (Pair K)<VAR>inst✝ : Field K<VAR>nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>g.convs (n + 1) = (g.squashGCF n).convs n
<VAR>K : Type u_1<VAR>n : ℕ<VAR>g : GenContFract K<VAR>s : Stream'.Seq (Pair K)<VAR>inst✝ : Field K<VAR>nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0<VAR>not_terminatedAt_n : ¬g.TerminatedAt n<GOAL>g.convs (n + 1) = (g.squashGCF n).convs n
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ p x : P<GOAL>x ∈ ↑(affineSpan k {p}) ↔ x ∈ {p}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ p x : P<GOAL>x -ᵥ p ∈ vectorSpan k {p} ↔ x ∈ {p}
<VAR>ψ θ : ℝ<GOAL>↑θ = ↑ψ ↔ ∃ k, θ - ψ = 2 * π * ↑k
<VAR>ψ θ : ℝ<GOAL>↑ψ = ↑θ ↔ ∃ k, θ - ψ = 2 * π * ↑k
<VAR>ψ θ : ℝ<GOAL>-ψ + θ ∈ AddSubgroup.zmultiples (2 * π) ↔ ∃ k, θ - ψ = 2 * π * ↑k
<VAR>x y : ℝ<VAR>a b : CauSeq ℚ abs<GOAL>{ cauchy := ⟦a ⊓ b⟧ } = Real.inf { cauchy := ⟦a⟧ } { cauchy := ⟦b⟧ }
<VAR>x y : ℝ<VAR>a b : CauSeq ℚ abs<GOAL>{ cauchy := ⟦a ⊓ b⟧ } = match { cauchy := ⟦a⟧ }, { cauchy := ⟦b⟧ } with | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun x x_1 => x ⊓ x_1) ⋯ x y }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<GOAL>borel α = MeasurableSpace.generateFrom (range Iio)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<GOAL>borel α ≤ MeasurableSpace.generateFrom (range Iio)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<GOAL>∀ t ∈ range Iio, MeasurableSet t
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<GOAL>a ≠ ⊤ → b ≠ ⊤ → a * b ≠ ⊤
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ✝ : σ ∈ alternatingGroup α<VAR>hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α<VAR>τ : Perm α<VAR>hτ : τ ∈ alternatingGroup α<VAR>hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩<GOAL>IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ✝ : σ ∈ alternatingGroup α<VAR>hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α<VAR>τ : Perm α<VAR>hτ : τ ∈ alternatingGroup α<VAR>hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩<VAR>π : Perm α<VAR>hπ : π * ↑⟨σ, hσ✝⟩ * π⁻¹ = ↑⟨τ, hτ⟩<GOAL>IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ✝ : σ ∈ alternatingGroup α<VAR>hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α<VAR>τ : Perm α<VAR>hτ : τ ∈ alternatingGroup α<VAR>hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩<VAR>π : Perm α<VAR>hπ : π * σ * π⁻¹ = τ<GOAL>IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ✝ : σ ∈ alternatingGroup α<VAR>hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α<VAR>τ : Perm α<VAR>hτ : τ ∈ alternatingGroup α<VAR>hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩<VAR>π : Perm α<VAR>hπ : π * σ * π⁻¹ = τ<VAR>h : sign π = 1<GOAL>IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ✝ : σ ∈ alternatingGroup α<VAR>hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α<VAR>τ : Perm α<VAR>hτ : τ ∈ alternatingGroup α<VAR>hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩<VAR>π : Perm α<VAR>hπ : π * σ * π⁻¹ = τ<VAR>h : sign π = -1<GOAL>IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set α<VAR>hc : s.Countable<VAR>hs : s.Nonempty<VAR>f : ℕ → ↑s<VAR>hf : Surjective f<GOAL>s = range (Subtype.val ∘ f)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<GOAL>Continuous f.vComp
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>this : Continuous ((fun x => (↑x, f.toFun x)) ∘ v.proj)<GOAL>Continuous f.vComp
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>this : Continuous ((fun x => (↑x, f.toFun x)) ∘ v.proj)<VAR>x : ℝ<GOAL>((fun x => (↑x, f.toFun x)) ∘ v.proj) x ∈ Icc v.tMin v.tMax ×ˢ closedBall v.x₀ ↑v.R
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>inst✝ : TopologicalSpace α<VAR>h : RestrictGenTopology 𝔖<GOAL>IsClosed {f | Continuous ((toFun 𝔖) f)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s✝ s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>inst✝ : TopologicalSpace α<VAR>h : RestrictGenTopology 𝔖<VAR>f : α →ᵤ[𝔖] β<VAR>u : Filter (α →ᵤ[𝔖] β)<VAR>x✝ : u.NeBot<VAR>hu : u ≤ 𝓟 {f | Continuous ((toFun 𝔖) f)}<VAR>huf : u ≤ 𝓝 f<VAR>s : Set α<VAR>hs : s ∈ 𝔖<GOAL>ContinuousOn ((toFun 𝔖) f) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s✝ s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>inst✝ : TopologicalSpace α<VAR>h : RestrictGenTopology 𝔖<VAR>f : α →ᵤ[𝔖] β<VAR>u : Filter (α →ᵤ[𝔖] β)<VAR>x✝ : u.NeBot<VAR>hu : u ≤ 𝓟 {f | Continuous ((toFun 𝔖) f)}<VAR>huf : ∀ s ∈ 𝔖, TendstoUniformlyOn (⇑(toFun 𝔖) ∘ id) ((toFun 𝔖) f) u s<VAR>s : Set α<VAR>hs : s ∈ 𝔖<GOAL>ContinuousOn ((toFun 𝔖) f) s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁶ : OrderedRing 𝕜<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t : Set E<VAR>x✝ y✝ : E<VAR>hs : StrictConvex 𝕜 s<VAR>f : E →ᵃ[𝕜] F<VAR>hf : IsOpenMap ⇑f<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : f x ≠ f y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • f x + b • f y ∈ interior (⇑f '' s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<GOAL>1 ≤ evenOdd Q 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<GOAL>1 ≤ LinearMap.range (ι Q) ^ ↑⟨0, ⋯⟩
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>inst✝ : Fintype ι<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>v : EuclideanSpace 𝕜 ι<GOAL>∑ i : ι, v i • b i = b.repr.symm v
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>inst✝ : Ring R<VAR>s : Set R<GOAL>(closure s).op = closure (MulOpposite.unop ⁻¹' s)
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>inst✝ : Ring R<VAR>s : Set R<GOAL>sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>inst✝ : Ring R<VAR>s : Set R<VAR>a : Subring Rᵐᵒᵖ<GOAL>a ∈ {a | s ⊆ MulOpposite.op ⁻¹' ↑a} ↔ a ∈ {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<GOAL>Tendsto (fun n => ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n) atTop (𝓝 0)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<GOAL>Tendsto (fun n => ‖Polynomial.eval a (Polynomial.derivative F)‖ * ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n) atTop (𝓝 (‖Polynomial.eval a (Polynomial.derivative F)‖ * 0))
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<GOAL>Tendsto (fun n => ‖Polynomial.eval a (Polynomial.derivative F)‖ * (‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n)) atTop (𝓝 (‖Polynomial.eval a (Polynomial.derivative F)‖ * 0))
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<GOAL>Tendsto (fun x => ‖Polynomial.eval a (Polynomial.derivative F)‖) atTop (𝓝 ‖Polynomial.eval a (Polynomial.derivative F)‖)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<GOAL>Tendsto (fun x => ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ x) atTop (𝓝 0)
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : Semiring R✝<VAR>p q : R✝[X]<VAR>S : Type u_2<VAR>inst✝³ : AddCommMonoid S<VAR>inst✝² : Pow S ℕ<VAR>inst✝¹ : Module R✝ S<VAR>x : S<VAR>R : Type u_3<VAR>inst✝ : Semiring R<VAR>r : R<GOAL>leval r = smeval.linearMap R r
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : Semiring R✝<VAR>p q : R✝[X]<VAR>S : Type u_2<VAR>inst✝³ : AddCommMonoid S<VAR>inst✝² : Pow S ℕ<VAR>inst✝¹ : Module R✝ S<VAR>x : S<VAR>R : Type u_3<VAR>inst✝ : Semiring R<VAR>r : R<GOAL>∀ (x : R[X]), (leval r) x = (smeval.linearMap R r) x
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : Semiring R✝<VAR>p q : R✝[X]<VAR>S : Type u_2<VAR>inst✝³ : AddCommMonoid S<VAR>inst✝² : Pow S ℕ<VAR>inst✝¹ : Module R✝ S<VAR>x : S<VAR>R : Type u_3<VAR>inst✝ : Semiring R<VAR>r : R<VAR>x✝ : R[X]<GOAL>(leval r) x✝ = (smeval.linearMap R r) x✝
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a c : α<VAR>h : c < 0<GOAL>(fun x => c * x) ⁻¹' Ioi a = Iio (a / c)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : CommRing 𝕜<VAR>inst✝⁶ : NoZeroDivisors 𝕜<VAR>inst✝⁵ : TopologicalSpace 𝕜<VAR>inst✝⁴ : ContinuousAdd 𝕜<VAR>inst✝³ : ContinuousConstSMul 𝕜 𝕜<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>φ ψ : ↑(characterSpace 𝕜 A)<VAR>h : RingHom.ker φ = RingHom.ker ψ<VAR>x : A<GOAL>φ x = ψ x