import examples.autodiff.generated.Quadratic import examples.autodiff.generated.JvpTangent import examples.autodiff.generated.Gradient import Mathlib.Analysis.Calculus.Deriv.Mul import Mathlib.Analysis.Calculus.Deriv.Addnamespace JaxLean.AutodiffUsed `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` theorem quadratic_hasDerivAt (x : ℝ) : HasDerivAt (fun y : ℝ => quadratic (Tensor.scalar y) ()) (2 * x + 3) x := byx:ℝ⊢ HasDerivAt (fun y => quadratic (Tensor.scalar y) ()) (2 * x + 3) x have h : HasDerivAt (fun y : ℝ => y * y + 3 * y) (1 * x + x * 1 + 3 * 1) x := ((hasDerivAt_id x).mul (hasDerivAt_id x)).add ((hasDerivAt_id x).const_mul 3)x:ℝh:HasDerivAt (fun y => y * y + 3 * y) (1 * x + x * 1 + 3 * 1) x⊢ HasDerivAt (fun y => quadratic (Tensor.scalar y) ()) (2 * x + 3) x convert h using 1e'_8x:ℝh:HasDerivAt (fun y => y * y + 3 * y) (1 * x + x * 1 + 3 * 1) x⊢ (fun y => quadratic (Tensor.scalar y) ()) = fun y => y * y + 3 * ye'_9x:ℝh:HasDerivAt (fun y => y * y + 3 * y) (1 * x + x * 1 + 3 * 1) x⊢ 2 * x + 3 = 1 * x + x * 1 + 3 * 1 <;>e'_8x:ℝh:HasDerivAt (fun y => y * y + 3 * y) (1 * x + x * 1 + 3 * 1) x⊢ (fun y => quadratic (Tensor.scalar y) ()) = fun y => y * y + 3 * ye'_9x:ℝh:HasDerivAt (fun y => y * y + 3 * y) (1 * x + x * 1 + 3 * 1) x⊢ 2 * x + 3 = 1 * x + x * 1 + 3 * 1 simp [quadratic, Tensor.scalar]e'_9x:ℝh:HasDerivAt (fun y => y * y + 3 * y) (1 * x + x * 1 + 3 * 1) x⊢ 2 * x = x + x Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`<;>e'_9x:ℝh:HasDerivAt (fun y => y * y + 3 * y) (1 * x + x * 1 + 3 * 1) x⊢ 2 * x = x + x ringAll goals completed! 🐙 theorem gradient_correct (x : ℝ) : gradient (Tensor.scalar x) () = deriv (fun y : ℝ => quadratic (Tensor.scalar y) ()) x := byx:ℝ⊢ gradient (Tensor.scalar x) () = deriv (fun y => quadratic (Tensor.scalar y) ()) x rw [(quadratic_hasDerivAt x).derivx:ℝ⊢ gradient (Tensor.scalar x) () = 2 * x + 3x:ℝ⊢ gradient (Tensor.scalar x) () = 2 * x + 3]x:ℝ⊢ gradient (Tensor.scalar x) () = 2 * x + 3 simp [gradient, Tensor.scalar]x:ℝ⊢ 3 + x + x = 2 * x + 3 ringAll goals completed! 🐙 theorem jvp_correct (x v : ℝ) : jvp_tangent (Tensor.scalar x) (Tensor.scalar v) () = deriv (fun y : ℝ => quadratic (Tensor.scalar y) ()) x * v := byx:ℝv:ℝ⊢ jvp_tangent (Tensor.scalar x) (Tensor.scalar v) () = deriv (fun y => quadratic (Tensor.scalar y) ()) x * v rw [(quadratic_hasDerivAt x).derivx:ℝv:ℝ⊢ jvp_tangent (Tensor.scalar x) (Tensor.scalar v) () = (2 * x + 3) * vx:ℝv:ℝ⊢ jvp_tangent (Tensor.scalar x) (Tensor.scalar v) () = (2 * x + 3) * v]x:ℝv:ℝ⊢ jvp_tangent (Tensor.scalar x) (Tensor.scalar v) () = (2 * x + 3) * v simp [jvp_tangent, Tensor.scalar]x:ℝv:ℝ⊢ v * x + x * v + 3 * v = (2 * x + 3) * v ringAll goals completed! 🐙 theorem certified_gradient_correct (x : ℝ) : Jaxpr.Program.eval (.cons (Tensor.scalar x) .nil) gradient_ir () = deriv (fun y : ℝ => Jaxpr.Program.eval (.cons (Tensor.scalar y) .nil) quadratic_ir ()) x := byx:ℝ⊢ Jaxpr.Program.eval (Jaxpr.Env.cons (Tensor.scalar x) Jaxpr.Env.nil) gradient_ir () = deriv (fun y => Jaxpr.Program.eval (Jaxpr.Env.cons (Tensor.scalar y) Jaxpr.Env.nil) quadratic_ir ()) x simp only [gradient_translation_correct, quadratic_translation_correct]x:ℝ⊢ gradient (Tensor.scalar x) () = deriv (fun y => quadratic (Tensor.scalar y) ()) x exact gradient_correct xAll goals completed! 🐙 theorem certified_jvp_correct (x v : ℝ) : Jaxpr.Program.eval (.cons (Tensor.scalar x) (.cons (Tensor.scalar v) .nil)) jvp_tangent_ir () = deriv (fun y : ℝ => Jaxpr.Program.eval (.cons (Tensor.scalar y) .nil) quadratic_ir ()) x * v := byx:ℝv:ℝ⊢ Jaxpr.Program.eval (Jaxpr.Env.cons (Tensor.scalar x) (Jaxpr.Env.cons (Tensor.scalar v) Jaxpr.Env.nil)) jvp_tangent_ir () = deriv (fun y => Jaxpr.Program.eval (Jaxpr.Env.cons (Tensor.scalar y) Jaxpr.Env.nil) quadratic_ir ()) x * v simp only [jvp_tangent_translation_correct, quadratic_translation_correct]x:ℝv:ℝ⊢ jvp_tangent (Tensor.scalar x) (Tensor.scalar v) () = deriv (fun y => quadratic (Tensor.scalar y) ()) x * v exact jvp_correct x vAll goals completed! 🐙end JaxLean.Autodiff