Type mismatch error with coercion

Stream: new members

[Park Sanghyeok]

I want to make a definition about complexity as follows.

import MIL.Common
import Mathlib.Topology.MetricSpace.Basic
import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
open MeasureTheory Set Metric

noncomputable def Complexity (X : Type*) [MeasurableSpace X] (F : Set (X → ℝ)) : ℕ :=
  sInf {n : ℕ | ∃ (A : (Fin n → X) → F),
                ∀ P : ProbabilityMeasure X,
                ∀t : Fin n → X,
                let f_out := A t
                P {x | (∫ x, f_out x ∂P) < 0.5}
                }

However, there's an error which says that

function expected at
  f_out
term has type
  ↑F

Also the tooltip says that A : (Fin n → X) → ↑F.
I don't know why we need coercion here.

If I change the definition above to below,

noncomputable def Complexity0 (X : Type*) [MeasurableSpace X] (F : Set (X → ℝ)) : ℕ :=
  sInf {n : ℕ | ∃ (A : (Fin n → X) → (X → ℝ)),
                ( ∀ t, A t ∈ F ) ∧
                (∀ P : ProbabilityMeasure X,
                ∀t : Fin n → X,
                let f_out := A t
                P {x | (∫ x, f_out x ∂P) < 0.5 }
                )
                }

then, error says that

type mismatch
  (fun s => ENNReal.toNNReal (↑↑↑P s)) {x | ∫ (x : X), f_out x ∂↑P < 0.5}
has type
  NNReal : Type
but is expected to have type
  Sort ?u.91192 : Type ?u.91192

I don't even know what ↑↑↑P means.

[Ruben Van de Velde]

So f_out is an element of ↑F, that is, the set F seen as a type. Replacing it by f_out.1 only makes me more confused, though

[Ruben Van de Velde]

You want the smallest n such that (mumble mumble) P { ... }

[Ruben Van de Velde]

But P { ... } is a number, not a proposition

[Park Sanghyeok]

Ruben Van de Velde 말함:

So f_out is an element of ↑F, that is, the set F seen as a type. Replacing it by f_out.1 only makes me more confused, though

I made a silly mistake, it was actually

P {x | (∫ x, f_out x ∂P) < 0.5 } < (0.5:ℝ)

And f_out.1 works fine. Thanks.
What does .1 means here?

[Ruben Van de Velde]

f_out is a pair of (function from X to \R, proof that that the function is in F), so f_out.1 is the function itself

[Ruben Van de Velde]

I'm not quite sure why it's needed

[Park Sanghyeok]

Ruben Van de Velde 말함:

f_out is a pair of (function from X to \R, proof that that the function is in F), so f_out.1 is the function itself

Thanks again.
In the notation f : X → Y, X and Y seem to be regarded only as a type.
I'm not sure the grammar for writing things like where the codomain is the set of functions...