theorem
proved
tactic proof
axisAdditive_linear
show as:
view Lean formalization →
formal statement (Lean)
127theorem axisAdditive_linear (f : ℕ → ℝ) (h : AxisAdditive f) :
128 ∀ d : ℕ, f d = (d : ℝ) * f 1 := by
proof body
Tactic-mode proof.
129 rcases h with ⟨h0, hadd⟩
130 intro d
131 induction d with
132 | zero =>
133 simp [h0]
134 | succ d ih =>
135 -- f(d+1) = f(d) + f(1)
136 have hstep : f (d + 1) = f d + f 1 := by
137 simpa using (hadd d 1)
138 -- expand and use IH
139 calc
140 f (Nat.succ d) = f d + f 1 := by
141 simpa [Nat.succ_eq_add_one] using hstep
142 _ = ((d : ℝ) * f 1) + f 1 := by simpa [ih]
143 _ = ((d : ℝ) + 1) * f 1 := by ring
144 _ = ((Nat.succ d : ℝ) * f 1) := by
145 simp [Nat.cast_succ, add_comm, add_left_comm, add_assoc]
146
147/-! ### Admissible correction terms -/
148
149/-- Admissible dimension correction: axis-additive and calibrated at D=3. -/