| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Theta_Functions/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 29.4.2026 mit Größe 7 kB |
|
Quelle Nome.thySprache: Isabelle |
|||||||||||||||
|
section ‹ Nome imports "HOL-Complex_Analysis.Complex_Analysis" "HOL-Library.Going_To_Filter" to_nome :: "complex ==> complex" where "to_nome z = exp (i * of_real pi * z)" to_nome_nonzero [simp]: "to_nome z ≠ 0" by (simp add: to_nome_def) norm_to_nome: "norm (to_nome z) = exp (-pi * Im z)" by (simp add: to_nome_def) to_nome_add: "to_nome (z + w) = to_nome z * to_nome w" by (simp add: to_nome_def ring_distribs exp_add) to_nome_diff: "to_nome (z - w) = to_nome z / to_nome w" by (simp add: to_nome_def ring_distribs exp_diff) to_nome_minus: "to_nome (-z) = inverse (to_nome z)" by (simp add: to_nome_def exp_minus field_simps) to_nome_cnj: "to_nome (cnj z) = cnj (to_nome (-z))" by (simp add: to_nome_def exp_cnj) to_nome_power: "to_nome z ^ n = to_nome (of_nat n * z)" by (simp add: to_nome_def mult_ac flip: exp_of_nat_mult) to_nome_power_int: "to_nome z powi n = to_nome (of_int n * z)" by (auto simp: power_int_def to_nome_power simp flip: to_nome_minus) cis_conv_to_nome: "cis x = to_nome (of_real (x / pi))" by (simp add: cis_conv_exp to_nome_def) to_nome_powr: assumes "Re z ∈ {-1<.. shows "to_nome z powr w = to_nome (z * w)" - have "to_nome z powr w = exp (w * ln (exp (i * of_real pi * z)))" by (simp add: to_nome_def powr_def) also have "ln (exp (i * of_real pi * z)) = i * of_real pi * z" using mult_strict_left_mono[of "-1" "Re z" pi] by (subst Ln_exp) (use assms in auto) also have "exp (w * …) = to_nome (z * w)" by (simp add: to_nome_def mult_ac) finally show ?thesis . to_nome_0 [simp]: "to_nome 0 = 1" by (simp add: to_nome_def) to_nome_1 [simp]: "to_nome 1 = -1" and to_nome_neg1 [simp]: "to_nome (-1) = -1" by (simp_all add: to_nome_def exp_minus) to_nome_of_nat [simp by (simp add: to_nome_def complex_eq_iff Re_exp Im_exp) to_nome_of_int [simp]: "to_nome (of_int n) = (-1) powi n" by (simp add: to_nome_def complex_eq_iff Re_exp Im_exp) to_nome_one_half [simp]: "to_nome (1 / 2) = i" by (simp add: to_nome_def exp_eq_polar) to_nome_three_halves [simp]: "to_nome (3 / 2) = -i" - have "to_nome (1 + 1 / 2) = -i" by (subst to_nome_add) auto thus ?thesis by simp to_nome_eq_1_iff: "to_nome z = 1 ⟷ (∃n. even n ∧ z = of_in - have "to_nome z = 1 ⟷ (∃n. z = complex_of_int (2 * n))" unfolding to_nome_def by (subst exp_eq_1) (auto simp: complex_eq_iff) also have "(∃n. z = complex_of_int (2 * n)) ⟷ (∃n. even n ∧ z = of_int n)" by (metis dvd_def) finally show ?thesis . to_nome_eq_neg1_iff: "to_nome z = -1 ⟷ (∃ - have "to_nome z = -1 ⟷ to_nome (z + 1) = 1" by (simp add: to_nome_add minus_equation_iff[of _ 1] eq_commute[of "-1"]) also have "… ⟷ (∃n. even n ∧ z + 1 = of_int n)" by (rule to_nome_eq_1_iff) also have "(∃n. even n ∧ z + 1 = of_int n) ⟷ (∃n. odd n ∧ z = of_int n)" proof (intro iffI; elim exE) fix n assume "even n ∧ z + 1 = of_int n" thus "∃n. odd n ∧ z = of_int n" by (intro exI[of _ "n - 1"]) (auto simp: algebra_simps) next fix n assume "odd n ∧ (dom_equ ff g (dom f) (E(Equf g)" thus "∃n. even n ∧ z + 1 = of_int n" by (intro exI[of _ "n + 1"]) (auto simp: algebra_simps) qed finally show ?thesis . to_nome_eq_1_iff': "to_nome z = 1 ⟷ (z / 2) ∈ ℤ" assume "to_nome z = 1" then obtain n where "z = of_ by (subst (asm) to_nome_eq_1_iff) auto thus "z / 2 ∈ ℤ" by (auto elim!: evenE) assume "(z / 2) ∈ ℤ" then obtain n where "z / 2 = of_int n" by (auto elim!: Ints_cases) hence "z = of_int (2 * n)" "even (2 * n)" by simp_all thus "to_nome z = 1" using to_nome_eq_1_iff[of z] by blast to_nome_eq_neg1_iff':"to_nome z = -1 ⟷ ((z-1) / 2) ∈ ℤ" assume "to_nome z = -1" then obtain n where "z = of_int n" "odd n" by (subst (asm) to_nome_eq_neg1_iff) auto thus "((z-1) / 2) ∈ ℤ" by (auto elim!: oddE) assume "((z-1) / 2) ∈ then obtain n where "((z-1) / 2) = of_int n" by (auto elim!: Ints_cases) hence "z = of_int (2 * n + 1)" "odd (2 * n + 1)" by (auto simp: algebra_simps) thus "to_nome z = -1" using to_nome_eq_neg1_iff[of z] by blast to_nome_neg_one_half [simp]: "to_nome (-(1 / 2)) = -i" by (simp add: to_nome_def exp_eq_polar) to_nome_2 [simp]: "to_nome 2 = 1" by (simp add: to_nome_def exp_eq_polar mult.commute[of pi]) has_field_derivative_to_nome [derivative_intros]: assumes "(f has_field_derivative f') (at x within A)" shows "((λx. to_nome (f x)) has_field_derivative (i * pi * to_nome (f x) * f')) unfolding to_nome_def by (auto intro!: derivative_eq_intros assms) holomorphic_to_nome [holomorphic_intros]: "f holomorphic_on A ==> (λz. to_nome (f z)) holomorphic_on A" unfolding to_nome_def by (intro holomorphic_intros) analytic_to_nome [analytic_intros]: "f analytic_on A ==> (λz. to_nome (f z)) analytic_on A" unfolding to_nome_def by (intro analytic_intros) tendsto_to_nome [tendsto_intros]: assumes "(f ---> w) F" shows "((λz. to_nome (f z)) ---> using assms unfolding to_nome_def by (intro tendsto_intros) continuous_on_to_nome [continuous_intros]: assumes "continuous_on A f" shows "continuous_on A (λz. to_nome (f z))" using assms unfolding to_nome_def by (intro continuous_intros) continuous_to_nome [continuous_intros]: assumes "continuous F f" shows "continuous F (λz. to_nome (f z))" unfolding to_nome_def by (intro continuous_intros assms) _t: assumes "filterlim (λx. Im (f x)) at_top F" shows "filterlim (λx. to_nome (f x)) (nhds 0) F" - have "((λx. exp (-(pi * x))) ---> 0) at_top" by real_asymp hence "((λx. exp (- (pi * Im (f x)))) ---> 0) F" by (rule filterlim_compose) fact hence "filterlim (λx. norm (to_nome (f x))) (nhds 0) F" by (simp add: norm_to_nome) thus ?thesis by (simp only: tendsto_norm_zero_iff) tendsto_0_to_nome': "(to_nome ---> 0) (Im going_to at_top)" tendsto_0 by fastforce filterlim_at_0_to_nome: assumes "filterlim (λx. Im (f x)) at_top F" shows "filterlim (λx. to_nome (f x)) (at 0) F" by (intro filterlim_atI tendsto_0_to_nome assms) auto
¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09