Variation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Finite total-variation operations used by the dependency-breaking argument. All statements concern the displayed real weight functions. In particular, conditioning rescales actual restricted weights, and kernels act by finite sums.

theorem OAI.UniqueGamesTheorem.Foundations.Repetition.totalVariation_triangle line 22
def OAI.UniqueGamesTheorem.Foundations.Repetition.conditionWeights line 34
Source documentation
The actual weights obtained by restricting to an event and normalizing.
```
noncomputable def conditionWeights (p : α → ℝ) (event : α → Bool) (z : ℝ) : α → ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.conditionWeights_isProbability line 37
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.totalVariation_condition_le line 56
Source documentation
Conditioning two laws on the same event of equal positive mass costs at most the inverse mass. The algebraic estimate itself needs no normalization.
```
theorem totalVariation_condition_le (p q : α → ℝ) (event : α → Bool)
    {z : ℝ} (hz : 0 < z) :
    totalVariation (conditionWeights p event z) (conditionWeights q event z) ≤
      totalVariation p q / z := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.conditionWeights
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.totalVariation_condition_half_le line 79

theorem OAI.UniqueGamesTheorem.Foundations.Repetition.totalVariation_append_kernel line 87

Source documentation

Appending the same conditional kernel preserves total variation exactly.

theorem totalVariation_append_kernel (p q : α → ℝ) (kernel : α → β → ℝ)
    (hk : ∀ a, IsProbability (kernel a)) :
    totalVariation (fun ab : α × β => p ab.1 * kernel ab.1 ab.2)
      (fun ab : α × β => q ab.1 * kernel ab.1 ab.2) = totalVariation p q := by
…

def OAI.UniqueGamesTheorem.Foundations.Repetition.kernelPushforward line 101
Source documentation
Applying a finite stochastic kernel, forgetting its input.
```
noncomputable def kernelPushforward (p : α → ℝ) (kernel : α → β → ℝ) : β → ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.totalVariation_kernelPushforward_le line 104