RecursiveProfiles.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The side and joint profiles count literal flips of the same raw input.

structure OAI.Paper320.NestedFamily line 13
Source documentation
Acceptance at a stronger index implies acceptance at every weaker index.
```
structure NestedFamily {h : ℕ} {I : Type}
    (F : Fin h → (I → Bool) → Bool) : Prop where
…
```
theorem OAI.Paper320.NestedFamily.rejects_of_le line 17
def OAI.Paper320.jointSensitivityAt line 27
Source documentation
The number of coordinates whose one-bit flip changes both predicates.
```
def jointSensitivityAt {I : Type} [Fintype I]
    (f g : (I → Bool) → Bool) (x : I → Bool) : ℕ :=
…
```
def OAI.Paper320.sideSensitivity line 33
Source documentation
Maximum sensitivity over all indices and inputs with the indicated output.
```
def sideSensitivity {h : ℕ} {I : Type} [Fintype I]
    (F : Fin h → (I → Bool) → Bool) (b : Bool) : ℕ :=
…
```
def OAI.Paper320.jointSensitivity line 39
Source documentation
Maximum same-input, same-bit joint sensitivity over two distinct ordered indices.
```
def jointSensitivity {h : ℕ} {I : Type} [Fintype I]
    (F : Fin h → (I → Bool) → Bool) (b : Bool) : ℕ :=
…
```
theorem OAI.Paper320.sensitivityAt_le_sideSensitivity line 45
theorem OAI.Paper320.sideSensitivity_le line 52
theorem OAI.Paper320.jointSensitivityAt_le_jointSensitivity line 64
theorem OAI.Paper320.jointSensitivity_le line 73
theorem OAI.Paper320.jointSensitivityAt_le_left line 87
theorem OAI.Paper320.jointSensitivityAt_comm line 94
theorem OAI.Paper320.jointSensitivity_one line 99