Perturbation.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

Sparse perturbations indexed by literal keys

A signature records the original bit and the actual key at every position. The key is never renamed. All positions with the same key use the same sampled bit. The finite events below therefore include the correlations caused by repeated keys, including inconsistent prescriptions.

abbrev OAI.QuantitativeVanDerWaerden.SparsePerturbation.Signature line 27
def OAI.QuantitativeVanDerWaerden.SparsePerturbation.usedKeys line 33
Source documentation
The actual key image of a literal signature.
```
noncomputable def usedKeys (σ : Signature Key k) : Finset Key := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.SparsePerturbation.Signature
def OAI.QuantitativeVanDerWaerden.SparsePerturbation.oppositePositions line 38
Source documentation
Positions whose original bit differs from the target bit.
```
def oppositePositions (σ : Signature Key k) (b : Bool) : Finset (Fin k) :=
…
```
Mentions: OAI.QuantitativeVanDerWaerden.SparsePerturbation.Signature
def OAI.QuantitativeVanDerWaerden.SparsePerturbation.oppositeKeys line 42
Source documentation
The fixed keys that must flip for the target event.
```
noncomputable def oppositeKeys (σ : Signature Key k) (b : Bool) : Finset Key := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.SparsePerturbation.Signature
def OAI.QuantitativeVanDerWaerden.SparsePerturbation.targetEvent line 47
Source documentation
The finite event that this signature becomes monochromatic in bit b.
```
noncomputable def targetEvent (σ : Signature Key k) (b : Bool) :
    Finset (Key → Bool) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.SparsePerturbation.Signature
theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.mem_targetEvent line 52
theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.xor_right_eq_of_same_target line 57
theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.xor_target_of_opposite line 61
theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.targetEvent_eq_empty_of_conflict line 66
Source documentation
A key shared by opposite original colors makes each target event empty.
```
theorem targetEvent_eq_empty_of_conflict (σ : Signature Key k) (b : Bool)
    {i j : Fin k} (hkey : (σ i).2 = (σ j).2) (hcolor : (σ i).1 ≠ (σ j).1) :
    targetEvent σ b = ∅ := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.SparsePerturbation.Signature, OAI.QuantitativeVanDerWaerden.SparsePerturbation.targetEvent
theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.targetEvent_eq_prescriptions line 82
Source documentation
A nonempty target event is exactly the cylinder prescribed by any one of its members, on the actual used-key set.
```
theorem targetEvent_eq_prescriptions (σ : Signature Key k) (b : Bool)
    {ω₀ : Key → Bool} (hω₀ : ω₀ ∈ targetEvent σ b) :
    targetEvent σ b = Finset.univ.filter (fun ω =>
      ∀ a ∈ usedKeys σ, ω a = ω₀ a) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.SparsePerturbation.Signature, OAI.QuantitativeVanDerWaerden.SparsePerturbation.targetEvent, OAI.QuantitativeVanDerWaerden.SparsePerturbation.usedKeys
theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.targetEvent_subset_opposite_cylinder line 100
Source documentation
Every target event forces the already determined opposite-key set to flip. There is no additional choice of a subset of keys.
```
theorem targetEvent_subset_opposite_cylinder (σ : Signature Key k) (b : Bool) :
    targetEvent σ b ⊆ Finset.univ.filter (fun ω =>
      ∀ a ∈ oppositeKeys σ b, ω a = true) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.SparsePerturbation.Signature, OAI.QuantitativeVanDerWaerden.SparsePerturbation.targetEvent, OAI.QuantitativeVanDerWaerden.SparsePerturbation.oppositeKeys
theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.targetEvent_eq_of_signature_eq line 112
Source documentation
The same literal signature gives the same event on the same key variables.
```
theorem targetEvent_eq_of_signature_eq {σ τ : Signature Key k} (h : σ = τ)
    (b : Bool) : targetEvent σ b = targetEvent τ b := by rw [h]
```
Mentions: OAI.QuantitativeVanDerWaerden.SparsePerturbation.Signature, OAI.QuantitativeVanDerWaerden.SparsePerturbation.targetEvent

theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.card_le_four_mul_card_image line 116

Source documentation

A multiplicity cap applies to every subset of positions.

theorem card_le_four_mul_card_image {Key : Type uKey} [Fintype Key] {k : ℕ}
    [DecidableEq Key]
    (σ : Signature Key k)
    (hmult : ∀ a, (Finset.univ.filter (fun j => (σ j).2 = a)).card ≤ 4)
    (J : Finset (Fin k)) :
    J.card ≤ 4 * (J.image (fun j => (σ j).2)).card := by
…

Mentions: OAI.QuantitativeVanDerWaerden.SparsePerturbation.Signature

theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.ceil_quarter_le_usedKeys_card line 136
Source documentation
Exact integer lower bound on the number of keys in a whole signature.
```
theorem ceil_quarter_le_usedKeys_card (σ : Signature Key k)
    (hmult : ∀ a, (Finset.univ.filter (fun j => (σ j).2 = a)).card ≤ 4) :
    (k + 3) / 4 ≤ (usedKeys σ).card := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.SparsePerturbation.Signature, OAI.QuantitativeVanDerWaerden.SparsePerturbation.usedKeys
theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.ceil_four_hundredth_le_oppositeKeys_card line 146
Source documentation
Exact integer lower bound on the predetermined flips in a rich signature. The richness premise is the integral form of at least k/100 opposite bits.
```
theorem ceil_four_hundredth_le_oppositeKeys_card (σ : Signature Key k) (b : Bool)
    (hmult : ∀ a, (Finset.univ.filter (fun j => (σ j).2 = a)).card ≤ 4)
    (hrich : k ≤ 100 * (oppositePositions σ b).card) :
    (k + 399) / 400 ≤ (oppositeKeys σ b).card := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.SparsePerturbation.Signature, OAI.QuantitativeVanDerWaerden.SparsePerturbation.oppositePositions, OAI.QuantitativeVanDerWaerden.SparsePerturbation.oppositeKeys
theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.target_probability_eq line 157
Source documentation
Exact target probability, whenever the prescriptions are consistent.
```
theorem target_probability_eq (p : ℝ) (σ : Signature Key k) (b : Bool)
    {ω₀ : Key → Bool} (hω₀ : ω₀ ∈ targetEvent σ b) :
    prob (bernoulliWeight p) (targetEvent σ b) =
      ∏ a ∈ usedKeys σ, if ω₀ a then p else 1 - p := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.SparsePerturbation.Signature, OAI.QuantitativeVanDerWaerden.SparsePerturbation.targetEvent, OAI.QuantitativeVanDerWaerden.SparsePerturbation.usedKeys
theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.target_probability_le_flip_pow line 166
Source documentation
Sparse flips preserve a fixed rich signature with high probability.
```
theorem target_probability_le_flip_pow {p : ℝ} (hp : 0 ≤ p) (hp1 : p ≤ 1)
    (σ : Signature Key k) (b : Bool) :
    prob (bernoulliWeight p) (targetEvent σ b) ≤ p ^ (oppositeKeys σ b).card := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.SparsePerturbation.Signature, OAI.QuantitativeVanDerWaerden.SparsePerturbation.targetEvent, OAI.QuantitativeVanDerWaerden.SparsePerturbation.oppositeKeys
theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.target_probability_le_stay_pow line 180
Source documentation
For p ≤ 1/2, every prescribed key has probability at most 1-p.
```
theorem target_probability_le_stay_pow {p : ℝ} (hp : 0 ≤ p) (hp2 : p ≤ 1 / 2)
    (σ : Signature Key k) (b : Bool) :
    prob (bernoulliWeight p) (targetEvent σ b) ≤ (1 - p) ^ (usedKeys σ).card := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.SparsePerturbation.Signature, OAI.QuantitativeVanDerWaerden.SparsePerturbation.targetEvent, OAI.QuantitativeVanDerWaerden.SparsePerturbation.usedKeys
theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.rich_target_probability_le line 198
theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.target_probability_le line 206
def OAI.QuantitativeVanDerWaerden.SparsePerturbation.monochromaticEvent line 215
Source documentation
Either target bit is bad.
```
noncomputable def monochromaticEvent (σ : Signature Key k) : Finset (Key → Bool) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.SparsePerturbation.Signature
theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.mem_monochromaticEvent line 219
theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.monochromatic_probability_le line 232

theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.exists_avoiding_of_rich_or_signature line 247

Source documentation

Finite sparse-perturbation theorem. The affine family is counted through its actual literal-signature image; repeated descriptions are not new events. No independence between different progression events is assumed.

theorem exists_avoiding_of_rich_or_signature {ι : Type uIndex} [DecidableEq ι]
    (P A : Finset ι) (σ : ι → Signature Key k) (hA : A ⊆ P)
    {p : ℝ} (hp : 0 ≤ p) (hp2 : p ≤ 1 / 2)
    (hmult : ∀ i ∈ P, ∀ a, (Finset.univ.filter (fun j => (σ i j).2 = a)).card ≤ 4)
    (hcases : ∀ i ∈ P, i ∈ A ∨ ∀ b, k ≤ 100 * (oppositePositions (σ i) b).card)
    (hbudget : 2 * (P.card : ℝ) * p ^ ((k + 399) / 400) +
      2 * ((A.image σ).card : ℝ) * (1 - p) ^ ((k + 3) / 4) < 1) :
    ∃ ω : Key → Bool, ∀ i ∈ P, ∀ b, ∃ j,
      Bool.xor (σ i j).1 (ω (σ i j).2) ≠ b := by
…

Mentions: OAI.QuantitativeVanDerWaerden.SparsePerturbation.Signature, OAI.QuantitativeVanDerWaerden.SparsePerturbation.oppositePositions

def OAI.QuantitativeVanDerWaerden.SparsePerturbation.nonzeroProgressions line 314
Source documentation
Actual ordered nonzero-step progressions in a finite cyclic group.
```
def nonzeroProgressions (N : ℕ) [NeZero N] : Finset (ZMod N × ZMod N) :=
…
```
theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.mem_nonzeroProgressions line 317
theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.nonzeroProgressions_card_le line 321
def OAI.QuantitativeVanDerWaerden.SparsePerturbation.cyclicSignature line 328
Source documentation
Literal signatures of the actual cyclic samples.
```
def cyclicSignature {N : ℕ} (c₀ : ZMod N → Bool) (key : ZMod N → Key)
    (ad : ZMod N × ZMod N) : Signature Key k :=
…
```
Mentions: OAI.QuantitativeVanDerWaerden.SparsePerturbation.Signature

theorem OAI.QuantitativeVanDerWaerden.SparsePerturbation.exists_cyclicAvoids_of_sparse_data line 334

Source documentation

Apply the finite product construction to the actual cyclic group. This wrapper constructs the coloring itself from the sampled key bits.

theorem exists_cyclicAvoids_of_sparse_data {N : ℕ} [NeZero N]
    (c₀ : ZMod N → Bool) (key : ZMod N → Key)
    (A : Finset (ZMod N × ZMod N)) (hA : A ⊆ nonzeroProgressions N)
    {p : ℝ} (hp : 0 ≤ p) (hp2 : p ≤ 1 / 2)
    (hmult : ∀ ad ∈ nonzeroProgressions N, ∀ a,
      (Finset.univ.filter (fun j : Fin k => (cyclicSignature (k := k) c₀ key ad j).2 = a)).card ≤ 4)
…

Mentions: OAI.QuantitativeVanDerWaerden.SparsePerturbation.nonzeroProgressions, OAI.QuantitativeVanDerWaerden.SparsePerturbation.cyclicSignature