Documentation

Lean 4 Proof

theorem euler_degree_one {J : ℕ} {F : (Fin J → ℝ) → ℝ}
    (hF : ∀ (x : Fin J → ℝ) (c : ℝ), c > 0 → F (fun j => c * x j) = c * F x)
    {x : Fin J → ℝ} {g' : ℝ}
    (hg : HasDerivAt (fun t => F (fun j => t * x j)) g' 1) :
    g' = F x := by
  -- F(t x) = t F(x) for t > 0, holds in a neighborhood of 1
  have heq : (fun t => F (fun j => t * x j)) =ᶠ[nhds (1 : ℝ)] (fun t => t * F x) :=
    Filter.eventually_iff_exists_mem.mpr ⟨Set.Ioi 0, Ioi_mem_nhds one_pos, fun t ht => hF x t ht⟩
  -- The linear function t -> t F(x) has derivative F(x) at t = 1
  have hlin : HasDerivAt (fun t : ℝ => t * F x) (F x) 1 := by
    have := (hasDerivAt_id (1 : ℝ)).mul_const (F x)
    simpa using this
  -- By uniqueness of derivatives (functions agree near 1)
  exact (heq.hasDerivAt_iff.mp hg).unique hlin

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:665

Module Section

Economics extensions for CES formalization:

In the same file