DirectionSampling.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Counting and avoiding all disjoint zero-tuple witnesses

All ordered tuples are retained, including tuples with repeated indices. The probability product estimate is applied only to lists whose distinct tuple supports are pairwise disjoint. Their number is bounded by the exact number of all ordered lists, u ^ (h * w).

theorem OAI.MetricEntropyDuality.DirectionSampling.prob_biUnion_le line 34
Source documentation
The union bound for the actual normalized finite sample counts.
```
theorem prob_biUnion_le (s : Finset J) (events : J → Finset (U → E)) :
    prob (s.biUnion events) ≤ ∑ j ∈ s, prob (events j) := by
…
```
theorem OAI.MetricEntropyDuality.DirectionSampling.exists_not_mem_of_prob_lt_one line 46
Source documentation
Strictly fewer than all samples in an event leaves an actual sample outside it. Nonempty E also covers an empty coordinate index type.
```
theorem exists_not_mem_of_prob_lt_one (event : Finset (U → E))
    (hevent : prob event < 1) : ∃ t : U → E, t ∉ event := by
…
```
theorem OAI.MetricEntropyDuality.DirectionSampling.tupleEvent_dependsOn line 65
Source documentation
A repeated-index tuple event depends only on the distinct indices in its literal support.
```
theorem tupleEvent_dependsOn (bad : (Fin h → E) → Prop) (a : Fin h → U) :
    DependsOn (tupleSupport a) (tupleEvent bad a) := by
…
```
Mentions: OAI.MetricEntropyDuality.tupleSupport, OAI.MetricEntropyDuality.tupleEvent
def OAI.MetricEntropyDuality.DirectionSampling.badListEvent line 74
Source documentation
The event that every tuple in this particular list is bad.
```
def badListEvent (bad : (Fin h → E) → Prop) (L : Fin w → Fin h → U) :
    Finset (U → E) :=
…
```
theorem OAI.MetricEntropyDuality.DirectionSampling.mem_badListEvent line 79
theorem OAI.MetricEntropyDuality.DirectionSampling.prob_badListEvent_le line 87
Source documentation
Product estimate proved from disjoint coordinate supports; no independence hypothesis is assumed.
```
theorem prob_badListEvent_le (bad : (Fin h → E) → Prop)
    (L : Fin w → Fin h → U) (hL : DisjointSupports L) (b : ℝ)
    (hbound : ∀ a : Fin h → U, prob (tupleEvent bad a) ≤ b) :
    prob (badListEvent bad L) ≤ b ^ w :=
…
```
Mentions: OAI.MetricEntropyDuality.DisjointSupports, OAI.MetricEntropyDuality.tupleEvent, OAI.MetricEntropyDuality.DirectionSampling.badListEvent
theorem OAI.MetricEntropyDuality.DirectionSampling.card_witnessLists line 99
Source documentation
All ordered witness lists, before imposing disjointness, are counted exactly. Repetition within any tuple remains allowed.
```
theorem card_witnessLists (u h w : ℕ) :
    Fintype.card (Fin w → Fin h → Fin u) = u ^ (h * w) := by
…
```
def OAI.MetricEntropyDuality.DirectionSampling.disjointLists line 104
Source documentation
Only disjoint lists are used as bad-event witnesses.
```
def disjointLists (u h w : ℕ) : Finset (Fin w → Fin h → Fin u) := by
…
```
theorem OAI.MetricEntropyDuality.DirectionSampling.mem_disjointLists line 108
theorem OAI.MetricEntropyDuality.DirectionSampling.card_disjointLists_le line 113
def OAI.MetricEntropyDuality.DirectionSampling.badSamples line 127
Source documentation
The actual union over forms and disjoint witness lists.
```
def badSamples (forms : Finset Z) (bad : Z → (Fin h → E) → Prop) :
    Finset (Fin u → E) := by
…
```
theorem OAI.MetricEntropyDuality.DirectionSampling.mem_badSamples line 134
theorem OAI.MetricEntropyDuality.DirectionSampling.prob_badSamples_le line 144
Source documentation
The counted union bound over the literal form set and every possible disjoint witness list.
```
theorem prob_badSamples_le (forms : Finset Z) (bad : Z → (Fin h → E) → Prop)
    (b : ℝ) (hb : 0 ≤ b)
    (hbound : ∀ z ∈ forms, ∀ a : Fin h → Fin u, prob (tupleEvent (bad z) a) ≤ b) :
    prob (badSamples (u := u) (w := w) forms bad) ≤
…
```
Mentions: OAI.MetricEntropyDuality.tupleEvent, OAI.MetricEntropyDuality.DirectionSampling.badSamples

theorem OAI.MetricEntropyDuality.DirectionSampling.exists_sample_avoiding line 175

Source documentation

A strict union budget produces one sample excluding every disjoint all-bad witness, simultaneously for every form in the actual finite set.

theorem exists_sample_avoiding (forms : Finset Z) (bad : Z → (Fin h → E) → Prop)
    (b : ℝ) (hb : 0 ≤ b)
    (hbound : ∀ z ∈ forms, ∀ a : Fin h → Fin u, prob (tupleEvent (bad z) a) ≤ b)
    (hbudget : (forms.card : ℝ) * (u : ℝ) ^ (h * w) * b ^ w < 1) :
    ∃ t : Fin u → E, ∀ z ∈ forms, ∀ L : Fin w → Fin h → Fin u,
      DisjointSupports L → ¬ ∀ j, bad z (fun i => t (L j i)) := by
…

Mentions: OAI.MetricEntropyDuality.tupleEvent, OAI.MetricEntropyDuality.DisjointSupports

theorem OAI.MetricEntropyDuality.DirectionSampling.prob_badSamples_le_field_budget line 191
Source documentation
The numerical bound used for degree-h forms over a field of p elements. Form counts and each repeated-tuple zero bound are explicit inputs, supplied by the actual form and polynomial constructions.
```
theorem prob_badSamples_le_field_budget (forms : Finset Z)
    (bad : Z → (Fin h → E) → Prop) (p D : ℕ) (hcard : forms.card ≤ p ^ D)
    (hbound : ∀ z ∈ forms, ∀ a : Fin h → Fin u,
      prob (tupleEvent (bad z) a) ≤ (h : ℝ) / p) :
    prob (badSamples (u := u) (w := w) forms bad) ≤
…
```
Mentions: OAI.MetricEntropyDuality.tupleEvent, OAI.MetricEntropyDuality.DirectionSampling.badSamples
theorem OAI.MetricEntropyDuality.DirectionSampling.exists_sample_avoiding_of_field_budget line 204