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 for acceptible answer declarations. Mathlib version used by the checker is v4.31.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