author paulson Thu Mar 05 17:30:29 2015 +0000 (2015-03-05) changeset 59613 7103019278f0 parent 59593 304ee0a475d1 child 59614 452458cf8506
The function frac. Various lemmas about limits, series, the exp function, etc.
 src/HOL/Archimedean_Field.thy file | annotate | diff | revisions src/HOL/Complex.thy file | annotate | diff | revisions src/HOL/Int.thy file | annotate | diff | revisions src/HOL/Limits.thy file | annotate | diff | revisions src/HOL/Real_Vector_Spaces.thy file | annotate | diff | revisions src/HOL/Series.thy file | annotate | diff | revisions src/HOL/Transcendental.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Archimedean_Field.thy	Thu Mar 05 11:11:42 2015 +0100
1.2 +++ b/src/HOL/Archimedean_Field.thy	Thu Mar 05 17:30:29 2015 +0000
1.3 @@ -150,6 +150,11 @@
1.4  lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> floor x = z"
1.5    using floor_correct [of x] floor_exists1 [of x] by auto
1.6
1.7 +lemma floor_unique_iff:
1.8 +  fixes x :: "'a::floor_ceiling"
1.9 +  shows  "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
1.10 +using floor_correct floor_unique by auto
1.11 +
1.12  lemma of_int_floor_le: "of_int (floor x) \<le> x"
1.13    using floor_correct ..
1.14
1.15 @@ -281,6 +286,9 @@
1.16  lemma floor_diff_of_int [simp]: "floor (x - of_int z) = floor x - z"
1.17    using floor_add_of_int [of x "- z"] by (simp add: algebra_simps)
1.18
1.19 +lemma floor_uminus_of_int [simp]: "floor (- (of_int z)) = - z"
1.20 +  by (metis floor_diff_of_int [of 0] diff_0 floor_zero)
1.21 +
1.22  lemma floor_diff_numeral [simp]:
1.23    "floor (x - numeral v) = floor x - numeral v"
1.24    using floor_diff_of_int [of x "numeral v"] by simp
1.25 @@ -464,4 +472,65 @@
1.26  lemma ceiling_minus: "ceiling (- x) = - floor x"
1.27    unfolding ceiling_def by simp
1.28
1.29 +subsection {* Frac Function *}
1.30 +
1.31 +
1.32 +definition frac :: "'a \<Rightarrow> 'a::floor_ceiling" where
1.33 +  "frac x \<equiv> x - of_int \<lfloor>x\<rfloor>"
1.34 +
1.35 +lemma frac_lt_1: "frac x < 1"
1.36 +  by  (simp add: frac_def) linarith
1.37 +
1.38 +lemma frac_eq_0_iff [simp]: "frac x = 0 \<longleftrightarrow> x \<in> Ints"
1.39 +  by (simp add: frac_def) (metis Ints_cases Ints_of_int floor_of_int )
1.40 +
1.41 +lemma frac_ge_0 [simp]: "frac x \<ge> 0"
1.42 +  unfolding frac_def
1.43 +  by linarith
1.44 +
1.45 +lemma frac_gt_0_iff [simp]: "frac x > 0 \<longleftrightarrow> x \<notin> Ints"
1.46 +  by (metis frac_eq_0_iff frac_ge_0 le_less less_irrefl)
1.47 +
1.48 +lemma frac_of_int [simp]: "frac (of_int z) = 0"
1.49 +  by (simp add: frac_def)
1.50 +
1.51 +lemma floor_add: "\<lfloor>x + y\<rfloor> = (if frac x + frac y < 1 then \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> else (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>) + 1)"
1.52 +proof -
1.53 +  {assume "x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)"
1.54 +   then have "\<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>"
1.56 +   }
1.57 +  moreover
1.58 +  { assume "\<not> x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)"
1.59 +    then have "\<lfloor>x + y\<rfloor> = 1 + (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>)"
1.60 +      apply (simp add: floor_unique_iff)
1.61 +      apply (auto simp add: algebra_simps)
1.62 +      by linarith
1.63 +  }
1.64 +  ultimately show ?thesis
1.65 +    by (auto simp add: frac_def algebra_simps)
1.66 +qed
1.67 +
1.68 +lemma frac_add: "frac (x + y) = (if frac x + frac y < 1 then frac x + frac y
1.69 +                                 else (frac x + frac y) - 1)"
1.70 +  by (simp add: frac_def floor_add)
1.71 +
1.72 +lemma frac_unique_iff:
1.73 +  fixes x :: "'a::floor_ceiling"
1.74 +  shows  "(frac x) = a \<longleftrightarrow> x - a \<in> Ints \<and> 0 \<le> a \<and> a < 1"
1.75 +  apply (auto simp: Ints_def frac_def)
1.76 +  apply linarith
1.77 +  apply linarith
1.78 +  by (metis (no_types) add.commute add.left_neutral eq_diff_eq floor_add_of_int floor_unique of_int_0)
1.79 +
1.80 +lemma frac_eq: "(frac x) = x \<longleftrightarrow> 0 \<le> x \<and> x < 1"
1.81 +  by (simp add: frac_unique_iff)
1.82 +
1.83 +lemma frac_neg:
1.84 +  fixes x :: "'a::floor_ceiling"
1.85 +  shows  "frac (-x) = (if x \<in> Ints then 0 else 1 - frac x)"
1.86 +  apply (auto simp add: frac_unique_iff)
1.87 +  apply (simp add: frac_def)
1.88 +  by (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq)
1.89 +
1.90  end
```
```     2.1 --- a/src/HOL/Complex.thy	Thu Mar 05 11:11:42 2015 +0100
2.2 +++ b/src/HOL/Complex.thy	Thu Mar 05 17:30:29 2015 +0000
2.3 @@ -73,7 +73,7 @@
2.4  definition "x / (y\<Colon>complex) = x * inverse y"
2.5
2.6  instance
2.7 -  by intro_classes
2.8 +  by intro_classes
2.9       (simp_all add: complex_eq_iff divide_complex_def
2.10        distrib_left distrib_right right_diff_distrib left_diff_distrib
2.11        power2_eq_square add_divide_distrib [symmetric])
2.12 @@ -161,6 +161,12 @@
2.13  lemma Im_complex_of_real [simp]: "Im (complex_of_real z) = 0"
2.14    by (simp add: of_real_def)
2.15
2.16 +lemma Re_divide_numeral [simp]: "Re (z / numeral w) = Re z / numeral w"
2.17 +  by (simp add: Re_divide sqr_conv_mult)
2.18 +
2.19 +lemma Im_divide_numeral [simp]: "Im (z / numeral w) = Im z / numeral w"
2.20 +  by (simp add: Im_divide sqr_conv_mult)
2.21 +
2.22  subsection {* The Complex Number \$i\$ *}
2.23
2.24  primcorec "ii" :: complex  ("\<i>") where
2.25 @@ -206,6 +212,9 @@
2.26  lemma complex_split_polar: "\<exists>r a. z = complex_of_real r * (cos a + \<i> * sin a)"
2.27    by (simp add: complex_eq_iff polar_Ex)
2.28
2.29 +lemma i_even_power [simp]: "\<i> ^ (n * 2) = (-1) ^ n"
2.30 +  by (metis mult.commute power2_i power_mult)
2.31 +
2.32  subsection {* Vector Norm *}
2.33
2.34  instantiation complex :: real_normed_field
2.35 @@ -501,11 +510,11 @@
2.36
2.37  lemma re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
2.38    by (auto simp add: Re_divide)
2.39 -
2.40 +
2.41  lemma im_complex_div_eq_0: "Im (a / b) = 0 \<longleftrightarrow> Im (a * cnj b) = 0"
2.42    by (auto simp add: Im_divide)
2.43
2.44 -lemma complex_div_gt_0:
2.45 +lemma complex_div_gt_0:
2.46    "(Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0) \<and> (Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0)"
2.47  proof cases
2.48    assume "b = 0" then show ?thesis by auto
2.49 @@ -547,7 +556,7 @@
2.50
2.51  lemma sums_complex_iff: "f sums x \<longleftrightarrow> ((\<lambda>x. Re (f x)) sums Re x) \<and> ((\<lambda>x. Im (f x)) sums Im x)"
2.52    unfolding sums_def tendsto_complex_iff Im_setsum Re_setsum ..
2.53 -
2.54 +
2.55  lemma summable_complex_iff: "summable f \<longleftrightarrow> summable (\<lambda>x. Re (f x)) \<and>  summable (\<lambda>x. Im (f x))"
2.56    unfolding summable_def sums_complex_iff[abs_def] by (metis complex.sel)
2.57
2.58 @@ -841,7 +850,7 @@
2.59      by auto
2.60  qed
2.61
2.62 -lemma csqrt_minus [simp]:
2.63 +lemma csqrt_minus [simp]:
2.64    assumes "Im x < 0 \<or> (Im x = 0 \<and> 0 \<le> Re x)"
2.65    shows "csqrt (- x) = \<i> * csqrt x"
2.66  proof -
```
```     3.1 --- a/src/HOL/Int.thy	Thu Mar 05 11:11:42 2015 +0100
3.2 +++ b/src/HOL/Int.thy	Thu Mar 05 17:30:29 2015 +0000
3.3 @@ -498,8 +498,16 @@
3.4  text{*Now we replace the case analysis rule by a more conventional one:
3.5  whether an integer is negative or not.*}
3.6
3.7 +text{*This version is symmetric in the two subgoals.*}
3.8 +theorem int_cases2 [case_names nonneg nonpos, cases type: int]:
3.9 +  "\<lbrakk>!! n. z = int n \<Longrightarrow> P;  !! n. z = - (int n) \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
3.10 +apply (cases "z < 0")
3.11 +apply (auto simp add: linorder_not_less dest!: negD nat_0_le [THEN sym])
3.12 +done
3.13 +
3.14 +text{*This is the default, with a negative case.*}
3.15  theorem int_cases [case_names nonneg neg, cases type: int]:
3.16 -  "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
3.17 +  "[|!! n. z = int n ==> P;  !! n. z = - (int (Suc n)) ==> P |] ==> P"
3.18  apply (cases "z < 0")
3.19  apply (blast dest!: negD)
3.20  apply (simp add: linorder_not_less del: of_nat_Suc)
```
```     4.1 --- a/src/HOL/Limits.thy	Thu Mar 05 11:11:42 2015 +0100
4.2 +++ b/src/HOL/Limits.thy	Thu Mar 05 17:30:29 2015 +0000
4.3 @@ -42,6 +42,11 @@
4.4    shows "filterlim f at_top F \<Longrightarrow> filterlim f at_infinity F"
4.5    by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl])
4.6
4.7 +lemma lim_infinity_imp_sequentially:
4.8 +  "(f ---> l) at_infinity \<Longrightarrow> ((\<lambda>n. f(n)) ---> l) sequentially"
4.9 +by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially)
4.10 +
4.11 +
4.12  subsubsection {* Boundedness *}
4.13
4.14  definition Bfun :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a filter \<Rightarrow> bool" where
4.15 @@ -885,7 +890,6 @@
4.16    qed
4.17  qed force
4.18
4.19 -
4.20  subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
4.21
4.22  text {*
4.23 @@ -1093,6 +1097,36 @@
4.24  lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) ---> 0) F"
4.25   by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
4.26
4.27 +
4.28 +lemma at_to_infinity:
4.29 +  fixes x :: "'a \<Colon> {real_normed_field,field_inverse_zero}"
4.30 +  shows "(at (0::'a)) = filtermap inverse at_infinity"
4.31 +proof (rule antisym)
4.32 +  have "(inverse ---> (0::'a)) at_infinity"
4.33 +    by (fact tendsto_inverse_0)
4.34 +  then show "filtermap inverse at_infinity \<le> at (0::'a)"
4.35 +    apply (simp add: le_principal eventually_filtermap eventually_at_infinity filterlim_def at_within_def)
4.36 +    apply (rule_tac x="1" in exI, auto)
4.37 +    done
4.38 +next
4.39 +  have "filtermap inverse (filtermap inverse (at (0::'a))) \<le> filtermap inverse at_infinity"
4.40 +    using filterlim_inverse_at_infinity unfolding filterlim_def
4.41 +    by (rule filtermap_mono)
4.42 +  then show "at (0::'a) \<le> filtermap inverse at_infinity"
4.43 +    by (simp add: filtermap_ident filtermap_filtermap)
4.44 +qed
4.45 +
4.46 +lemma lim_at_infinity_0:
4.47 +  fixes l :: "'a :: {real_normed_field,field_inverse_zero}"
4.48 +  shows "(f ---> l) at_infinity \<longleftrightarrow> ((f o inverse) ---> l) (at (0::'a))"
4.49 +by (simp add: tendsto_compose_filtermap at_to_infinity filtermap_filtermap)
4.50 +
4.51 +lemma lim_zero_infinity:
4.52 +  fixes l :: "'a :: {real_normed_field,field_inverse_zero}"
4.53 +  shows "((\<lambda>x. f(1 / x)) ---> l) (at (0::'a)) \<Longrightarrow> (f ---> l) at_infinity"
4.54 +by (simp add: inverse_eq_divide lim_at_infinity_0 comp_def)
4.55 +
4.56 +
4.57  text {*
4.58
4.59  We only show rules for multiplication and addition when the functions are either against a real
```
```     5.1 --- a/src/HOL/Real_Vector_Spaces.thy	Thu Mar 05 11:11:42 2015 +0100
5.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Thu Mar 05 17:30:29 2015 +0000
5.3 @@ -853,6 +853,12 @@
5.4    shows "norm (x ^ n) = norm x ^ n"
5.5  by (induct n) (simp_all add: norm_mult)
5.6
5.7 +text{*Despite a superficial resemblance, @{text norm_eq_1} is not relevant.*}
5.8 +lemma square_norm_one:
5.9 +  fixes x :: "'a::real_normed_div_algebra"
5.10 +  assumes "x^2 = 1" shows "norm x = 1"
5.11 +  by (metis assms norm_minus_cancel norm_one power2_eq_1_iff)
5.12 +
5.13  lemma setprod_norm:
5.14    fixes f :: "'a \<Rightarrow> 'b::{comm_semiring_1,real_normed_div_algebra}"
5.15    shows "setprod (\<lambda>x. norm(f x)) A = norm (setprod f A)"
```
```     6.1 --- a/src/HOL/Series.thy	Thu Mar 05 11:11:42 2015 +0100
6.2 +++ b/src/HOL/Series.thy	Thu Mar 05 17:30:29 2015 +0000
6.3 @@ -125,6 +125,11 @@
6.4  lemma sums_iff: "f sums x \<longleftrightarrow> summable f \<and> (suminf f = x)"
6.5    by (metis summable_sums sums_summable sums_unique)
6.6
6.7 +lemma sums_unique2:
6.8 +  fixes a b :: "'a::{comm_monoid_add,t2_space}"
6.9 +  shows "f sums a \<Longrightarrow> f sums b \<Longrightarrow> a = b"
6.10 +by (simp add: sums_iff)
6.11 +
6.12  lemma suminf_finite:
6.13    assumes N: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
6.14    shows "suminf f = (\<Sum>n\<in>N. f n)"
6.15 @@ -316,6 +321,12 @@
6.16
6.17  end
6.18
6.19 +lemma summable_minus_iff:
6.20 +  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
6.21 +  shows "summable (\<lambda>n. - f n) \<longleftrightarrow> summable f"
6.22 +  by (auto dest: summable_minus) --{*used two ways, hence must be outside the context above*}
6.23 +
6.24 +
6.25  context
6.26    fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::real_normed_vector" and I :: "'i set"
6.27  begin
```
```     7.1 --- a/src/HOL/Transcendental.thy	Thu Mar 05 11:11:42 2015 +0100
7.2 +++ b/src/HOL/Transcendental.thy	Thu Mar 05 17:30:29 2015 +0000
7.3 @@ -1011,22 +1011,22 @@
7.4    by (rule DERIV_exp [THEN DERIV_isCont])
7.5
7.6  lemma isCont_exp' [simp]:
7.7 -  fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
7.8 +  fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
7.9    shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. exp (f x)) a"
7.10    by (rule isCont_o2 [OF _ isCont_exp])
7.11
7.12  lemma tendsto_exp [tendsto_intros]:
7.13 -  fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
7.14 +  fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
7.15    shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F"
7.16    by (rule isCont_tendsto_compose [OF isCont_exp])
7.17
7.18  lemma continuous_exp [continuous_intros]:
7.19 -  fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
7.20 +  fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
7.21    shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
7.22    unfolding continuous_def by (rule tendsto_exp)
7.23
7.24  lemma continuous_on_exp [continuous_intros]:
7.25 -  fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
7.26 +  fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
7.27    shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))"
7.28    unfolding continuous_on_def by (auto intro: tendsto_exp)
7.29
7.30 @@ -1106,6 +1106,9 @@
7.31    shows "exp (x + y) = exp x * exp y"
7.32    by (rule exp_add_commuting) (simp add: ac_simps)
7.33
7.34 +lemma exp_double: "exp(2 * z) = exp z ^ 2"
7.35 +  by (simp add: exp_add_commuting mult_2 power2_eq_square)
7.36 +
7.37  lemmas mult_exp_exp = exp_add [symmetric]
7.38
7.39  lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
7.40 @@ -1136,6 +1139,14 @@
7.41    shows "exp (x - y) = exp x / exp y"
7.42    using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
7.43
7.44 +lemma exp_of_nat_mult:
7.45 +  fixes x :: "'a::{real_normed_field,banach}"
7.46 +  shows "exp(of_nat n * x) = exp(x) ^ n"
7.47 +    by (induct n) (auto simp add: distrib_left exp_add mult.commute)
7.48 +
7.49 +lemma exp_setsum: "finite I \<Longrightarrow> exp(setsum f I) = setprod (\<lambda>x. exp(f x)) I"
7.50 +  by (induction I rule: finite_induct) (auto simp: exp_add_commuting mult.commute)
7.51 +
7.52
7.53  subsubsection {* Properties of the Exponential Function on Reals *}
7.54
7.55 @@ -1160,9 +1171,10 @@
7.56  lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x"
7.57    by simp
7.58
7.59 -lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
7.60 +(*FIXME: superseded by exp_of_nat_mult*)
7.61 +lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
7.62    by (induct n) (auto simp add: real_of_nat_Suc distrib_left exp_add mult.commute)
7.63 -
7.64 +
7.65  text {* Strict monotonicity of exponential. *}
7.66
7.68 @@ -1481,6 +1493,36 @@
7.69    thus ?thesis unfolding exp_first_two_terms by auto
7.70  qed
7.71
7.72 +corollary exp_half_le2: "exp(1/2) \<le> (2::real)"
7.73 +  using exp_bound [of "1/2"]
7.74 +  by (simp add: field_simps)
7.75 +
7.76 +lemma exp_bound_half: "norm(z) \<le> 1/2 \<Longrightarrow> norm(exp z) \<le> 2"
7.77 +  by (blast intro: order_trans intro!: exp_half_le2 norm_exp)
7.78 +
7.79 +lemma exp_bound_lemma:
7.80 +  assumes "norm(z) \<le> 1/2" shows "norm(exp z) \<le> 1 + 2 * norm(z)"
7.81 +proof -
7.82 +  have n: "(norm z)\<^sup>2 \<le> norm z * 1"
7.83 +    unfolding power2_eq_square
7.84 +    apply (rule mult_left_mono)
7.85 +    using assms
7.86 +    apply (auto simp: )
7.87 +    done
7.88 +  show ?thesis
7.89 +    apply (rule order_trans [OF norm_exp])
7.90 +    apply (rule order_trans [OF exp_bound])
7.91 +    using assms n
7.92 +    apply (auto simp: )
7.93 +    done
7.94 +qed
7.95 +
7.96 +lemma real_exp_bound_lemma:
7.97 +  fixes x :: real
7.98 +  shows "0 \<le> x \<Longrightarrow> x \<le> 1/2 \<Longrightarrow> exp(x) \<le> 1 + 2 * x"
7.99 +using exp_bound_lemma [of x]
7.100 +by simp
7.101 +
7.102  lemma ln_one_minus_pos_upper_bound: "0 <= x \<Longrightarrow> x < 1 \<Longrightarrow> ln (1 - x) <= - x"
7.103  proof -
7.104    assume a: "0 <= (x::real)" and b: "x < 1"
7.105 @@ -1736,6 +1778,16 @@
7.106    by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="ln"])
7.107       (auto intro: eventually_gt_at_top)
7.108
7.109 +lemma lim_exp_minus_1:
7.110 +  fixes x :: "'a::{real_normed_field,banach}"
7.111 +  shows "((\<lambda>z::'a. (exp(z) - 1) / z) ---> 1) (at 0)"
7.112 +proof -
7.113 +  have "((\<lambda>z::'a. exp(z) - 1) has_field_derivative 1) (at 0)"
7.114 +    by (intro derivative_eq_intros | simp)+
7.115 +  then show ?thesis
7.116 +    by (simp add: Deriv.DERIV_iff2)
7.117 +qed
7.118 +
7.119  lemma ln_at_0: "LIM x at_right 0. ln x :> at_bot"
7.120    by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
7.121       (auto simp: eventually_at_filter)
```