Model.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Literal Boolean flips and ordinary sensitivity measures. All maxima range over the actual finite input or block-family space.

def OAI.Paper320.flip line 14
Source documentation
Flip exactly the coordinates belonging to the specified block.
Also declared: ComparatorChallenges/SensitivitySeparation.lean:10 (same declaration text).
```
def flip {I : Type} (x : I → Bool) (B : Finset I) : I → Bool :=
…
```
def OAI.Paper320.sensitivityAt line 18
Source documentation
The ordinary number of sensitive individual input coordinates.
Also declared: ComparatorChallenges/SensitivitySeparation.lean:13 (same declaration text).
```
def sensitivityAt {I : Type} [Fintype I]
    (f : (I → Bool) → Bool) (x : I → Bool) : ℕ :=
…
```
def OAI.Paper320.sensitivity line 23
Source documentation
Maximum ordinary sensitivity over all Boolean inputs.
Also declared: ComparatorChallenges/SensitivitySeparation.lean:17 (same declaration text).
```
def sensitivity {I : Type} [Fintype I] (f : (I → Bool) → Bool) : ℕ :=
…
```
def OAI.Paper320.blockSensitivityAt line 28
Source documentation
Maximum size of a family of disjoint nonempty sensitive blocks at an input. The empty family is allowed and contributes zero. Invalid families contribute zero.
Also declared: ComparatorChallenges/SensitivitySeparation.lean:20 (same declaration text).
```
def blockSensitivityAt {I : Type} [Fintype I]
    (f : (I → Bool) → Bool) (x : I → Bool) : ℕ :=
…
```
def OAI.Paper320.blockSensitivity line 36
Source documentation
Maximum block sensitivity over all Boolean inputs.
Also declared: ComparatorChallenges/SensitivitySeparation.lean:27 (same declaration text).
```
def blockSensitivity {I : Type} [Fintype I] (f : (I → Bool) → Bool) : ℕ :=
…
```