UniformRestriction.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Uniform restriction of Boolean tapes

Restricting a uniformly sampled Boolean function to a decidable subset gives the uniform law on functions on that subset. The subset and its complement may be empty: their Boolean function spaces still contain the constant-false function. Extending by false gives a canonical full-domain oracle address.

def OAI.MaxCutGames.Foundations.PCP.UniformRestriction.restrict line 22
Source documentation
The values of a full Boolean tape on the legal coordinates.
```
def restrict (f : B → Bool) : {b // p b} → Bool := fun b => f b.1
…
```
def OAI.MaxCutGames.Foundations.PCP.UniformRestriction.extend line 27
Source documentation
Extend a tape on legal coordinates by false on every other coordinate.
```
def extend (g : {b // p b} → Bool) : B → Bool :=
…
```
def OAI.MaxCutGames.Foundations.PCP.UniformRestriction.canonicalize line 31
Source documentation
Replace the values outside the legal coordinates by false.
```
def canonicalize (f : B → Bool) : B → Bool := extend p (restrict p f)
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.UniformRestriction.extend, OAI.MaxCutGames.Foundations.PCP.UniformRestriction.restrict
theorem OAI.MaxCutGames.Foundations.PCP.UniformRestriction.restrict_apply line 34
theorem OAI.MaxCutGames.Foundations.PCP.UniformRestriction.extend_apply_of_mem line 37
theorem OAI.MaxCutGames.Foundations.PCP.UniformRestriction.extend_apply_of_not_mem line 41
theorem OAI.MaxCutGames.Foundations.PCP.UniformRestriction.restrict_extend line 45
theorem OAI.MaxCutGames.Foundations.PCP.UniformRestriction.canonicalize_apply_of_mem line 50
theorem OAI.MaxCutGames.Foundations.PCP.UniformRestriction.canonicalize_apply_of_not_mem line 54
theorem OAI.MaxCutGames.Foundations.PCP.UniformRestriction.restrict_canonicalize line 58
theorem OAI.MaxCutGames.Foundations.PCP.UniformRestriction.canonicalize_idempotent line 62
theorem OAI.MaxCutGames.Foundations.PCP.UniformRestriction.canonicalize_eq_iff line 66
theorem OAI.MaxCutGames.Foundations.PCP.UniformRestriction.expect_restrict line 77
Source documentation
Uniform full tapes induce exactly uniform legal-coordinate tapes.
```
theorem expect_restrict (h : ({b // p b} → Bool) → ℝ) :
    (𝔼 f : B → Bool, h (restrict p f)) = 𝔼 g : {b // p b} → Bool, h g := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.UniformRestriction.restrict
theorem OAI.MaxCutGames.Foundations.PCP.UniformRestriction.expect_canonicalize line 94
Source documentation
The same law after choosing the canonical full-domain oracle address.
```
theorem expect_canonicalize (h : (B → Bool) → ℝ) :
    (𝔼 f : B → Bool, h (canonicalize p f)) =
      𝔼 g : {b // p b} → Bool, h (extend p g) :=
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.UniformRestriction.canonicalize, OAI.MaxCutGames.Foundations.PCP.UniformRestriction.extend

theorem OAI.MaxCutGames.Foundations.PCP.UniformRestriction.expect_restrict_pair line 100

Source documentation

Two independent full tapes restrict to two independent uniform legal tapes.

theorem expect_restrict_pair (h : ({b // p b} → Bool) → ({b // p b} → Bool) → ℝ) :
    (𝔼 f : B → Bool, 𝔼 g : B → Bool, h (restrict p f) (restrict p g)) =
      𝔼 f : {b // p b} → Bool, 𝔼 g : {b // p b} → Bool, h f g := by
…

Mentions: OAI.MaxCutGames.Foundations.PCP.UniformRestriction.restrict