Documentation

Lean 4 Proof

theorem tangentSpace_is_onePerp (hJ : 0 < J) (v : Fin J → ℝ) :
    (1 / (↑J : ℝ)) * vecSum J v = 0 ↔ orthToOne J v := by
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  simp only [orthToOne]
  constructor
  · intro h; simpa [mul_eq_zero, Nat.cast_ne_zero.mpr (by omega : J ≠ 0)] using h
  · intro h; rw [h, mul_zero]

Dependency Graph

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:47

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file