2021 OMA Intercolegial Level 2 Problem 1

The average of 16 numbers is equal to 168 . The numbers are modified as follows: 3 is subtracted from each of the first 8 numbers and 10 is added to each of the last 8 numbers. Determine the value of the average of the 16 numbers obtained.

_Replace_ `sorry` _in the template below with your solution. See [Answer Bank](index.php?action=view_answers) for acceptible answer declarations. Mathlib version used by the checker is v4.28.0_.

import Mathlib.Analysis.RCLike.Basic

def answer : ℝ := sorry

noncomputable
def List.Vector.mean (v : List.Vector ℝ 16) : ℝ :=
  v.toList.sum / 16

def List.Vector.modify (v : List.Vector ℝ 16) : List.Vector ℝ 16 :=
  List.Vector.ofFn <| fun i ↦
    if i < 8 then
      v.get i - 3
    else
      v.get i + 10

theorem solution : ∀ v : List.Vector ℝ 16, v.mean = 168 → (v.modify).mean = answer := sorry

Submit Solution

Login to submit a solution.

Recent Submissions