PutnamBench

putnam_1981_a1

abbrev putnam_1981_a1_solution : ℝ := sorry -- 1/8 theorem putnam_1981_a1 (P : ℕ → ℕ → Prop := fun n k : ℕ => 5^k ∣ ∏ m in Finset.Icc 1 n, (m^m : ℤ)) (E : ℕ → ℕ) (hE : ∀ n ∈ Ici 1, P n (E n) ∧ ∀ k : ℕ, P n k → k ≤ E n) : Tendsto (fun n : ℕ => ((E n) : ℝ)/n^2) atTop (𝓝 putnam_1981_a1_solution) := sorry

Let $E(n)$ be the greatest integer $k$ such that $5^k$ divides $1^1 2^2 3^3 \cdots n^n$. Find $\lim_{n \rightarrow \infty} \frac{E(n)}{n^2}$.

The limit equals $\frac{1}{8}$.

['analysis', 'number_theory']

Section putnam_1981_a1. Require Import Nat Reals Coquelicot.Coquelicot. From mathcomp Require Import div. Definition putnam_1981_a1_solution := 1 / 8. Theorem putnam_1981_a1 (prod_n : (nat -> nat) -> nat -> nat := fix prod_n (m: nat -> nat) (n : nat) := match n with | O => m 0%nat | S n' => mul (m n') (prod_n m n') end) (P : nat -> nat -> Prop := fun n k => 5 ^ k %| prod_n (fun m => Nat.pow m m) (S n) = true) (f : nat -> nat) (hf : forall (n: nat), gt n 1 -> P n (f n) /\ forall (k: nat), P n k -> le k (f n)) : Lim_seq (fun n => INR (f n) / INR n …

theory putnam_1981_a1 imports Complex_Main begin definition putnam_1981_a1_solution::real where "putnam_1981_a1_solution \<equiv> undefined" (* 1/8 *) theorem putnam_1981_a1: fixes P::"nat\<Rightarrow>nat\<Rightarrow>bool" and E::"nat\<Rightarrow>nat" defines "P \<equiv> \<lambda>n. \<lambda>k. 5^k dvd (\<Prod>m=1..n. m^m)" and "E \<equiv> \<lambda>n. (GREATEST k. P n k)" shows "(\<lambda>n. (E n) / n^2) \<longlonglongrightarrow> putnam_1981_a1_solution" sorry end

putnam_1981_a3

abbrev putnam_1981_a3_solution : Prop := sorry -- False theorem putnam_1981_a3 (f : ℝ → ℝ := fun t : ℝ => Real.exp (-t) * ∫ y in (Ico 0 t), ∫ x in (Ico 0 t), (Real.exp x - Real.exp y) / (x - y)) : (∃ L : ℝ, Tendsto f atTop (𝓝 L)) ↔ putnam_1981_a3_solution := sorry

Does the limit $$lim_{t \rightarrow \infty}e^{-t}\int_{0}^{t}\int_{0}^{t}\frac{e^x - e^y}{x - y} dx dy$$exist?

The limit does not exist.

['analysis']

Section putnam_1981_a3. Require Import Reals Coquelicot.Coquelicot. Definition putnam_1981_a3_solution := 14. Theorem putnam_1981_a3: Lim_seq (fun k => exp (-1*INR k) * (RInt (fun x => (RInt (fun y => (exp x - exp y) / (x - y)) 0 (INR k))) 0 (INR k))) = putnam_1981_a3_solution. Proof. Admitted. End putnam_1981_a3.

theory putnam_1981_a3 imports Complex_Main "HOL-Analysis.Interval_Integral" begin definition putnam_1981_a3_solution::bool where "putnam_1981_a3_solution \<equiv> undefined" (* False *) theorem putnam_1981_a3: fixes f::"real\<Rightarrow>real" defines "f \<equiv> \<lambda>t::real. exp (-t) * interval_lebesgue_integral lebesgue 0 t (\<lambda>y::real. interval_lebesgue_integral lebesgue 0 t (\<lambda>x::real. (exp x - exp y) / (x - y)))" shows "(\<exists>L::real. (f \<longlonglongrightarrow> L)) \<longleftrightarrow> putnam_1981_a3_solution" sorry end