Documentation

Lean 4 Proof

theorem portfolio_diversification (J : ℕ) (hJ : 0 < J) (s_sq g : ℝ) :
    s_sq / ↑J + (↑J - 1) / ↑J * g = (s_sq - g) / ↑J + g := by
  have hJr : (0 : ℝ) < ↑J := Nat.cast_pos.mpr hJ
  field_simp
  ring

Dependency Graph

Location

thesis/CESProofs/Dynamics/ConservationLaws.lean:213

Module Section

Results 36-46: Conservation Laws and Symmetry Identities

In the same file