Compfiles/Imo2019P1.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

3 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2019, Problem 1

Let ℤ be the set of integers. Determine all functions f : ℤ → ℤ such that, for all integers a and b,

f(2 * a) + 2 * f(b) = f(f(a + b)).

Imports (2)
Imported by 1 file
  1. lemma Imo2019P1.additive_to_int_linear proof of the following lemma suggested on Zulip by Riccardo Brasca line 29 source

    Source comment

    proof of the following lemma suggested on Zulip by Riccardo Brasca

    standard axioms: propext what this means

    Statement uses: Int, Eq, HAdd.hAdd, Exists, HMul.hMul

    Proof uses: LinearMap, RingHom.id, AddMonoidHom.toIntLinearMap, AddMonoidHom.mk', Exists.intro, OfNat.ofNat, id, Eq.symm, Module.Dual, Dual.apply_one_mul_eq

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

    lemma additive_to_int_linear (f : ℤ → ℤ) (h: ∀ (x y : ℤ), f (x + y) = f x + f y):
   ∃ c, ∀ a, f a = c * a := by
…

    Mentions: f, h

  2. determine Imo2019P1.solution_set line 38 source

    no axioms what this means

    Statement uses: Set, Int

    Proof uses: Set.ofPred, Or, Eq, OfNat.ofNat, Exists, HAdd.hAdd, HMul.hMul

    5 instances, coercions and auxiliary constants left out.

  3. problem Imo2019P1.imo2019_p1 IMO 2019 Problem 1: a functional equation on the integers line 41 source

    L4DEL explanation

    The integer functions with f(2a) + 2f(b) = f(f(a+b)) are exactly the zero function and f(z) = 2z + c.

    1. Problem: determine all f from the integers to the integers with f(2a) + 2f(b) = f(f(a+b)) for all integers a, b. The formal answer is the determined set solution_set = zero function or z to 2z + c for some integer c, and the theorem says f satisfies the equation iff f is in that set.
    2. Solution (complete, no sorry): the reverse direction is a direct computation.
    3. Forward direction: g(z) = f(z) - f(0) is additive, hence linear g(z) = d * z (lemma additive_to_int_linear), so f(z) = d * z + f(0).
    4. Substituting back into the equation splits into d = 0, which forces f(0) = 0 and so f = 0, and d not 0, which ends with f(z) = 2z + f(0), so f(0) is the free constant.

    Prerequisites: Imo2019P1.solution_set

    Sources and attribution: Pinned Lean source (47b19bbfe5f3)

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Int, Iff, Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Membership.mem, Set, Imo2019P1.solution_set

    Proof uses: Iff.intro, HSub.hSub, Eq.refl, Eq.mpr, id, congr, congrArg, Eq.mp, congrFun', MulZeroClass.mul_zero, zero_add, add_zero, Exists, Imo2019P1.additive_to_int_linear, Eq.symm, sub_add_cancel, dite, Or.inl, Eq.trans, MulZeroClass.zero_mul and 50 more

    86 instances, coercions and auxiliary constants left out.

    Tactic trace: 57 steps

    Open to load the checked before-and-after goal states.

    problem imo2019_p1 (f : ℤ → ℤ) :
    (∀ a b, f (2 * a) + 2 * (f b) = f (f (a + b))) ↔ f ∈ solution_set := by
…

    Mentions: f, Imo2019P1.solution_set