Arrangement.lean`

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.QuantitativeVanDerWaerden.AffineForm line 27
Source documentation
A real affine form in e parameters.
```
structure AffineForm (e : ℕ) where
…
```
def OAI.QuantitativeVanDerWaerden.AffineForm.eval line 31
def OAI.QuantitativeVanDerWaerden.signVector line 34
def OAI.QuantitativeVanDerWaerden.realizedSigns line 38
Source documentation
Realized patterns on any specified parameter subset.
```
def realizedSigns {e s : ℕ} (forms : Fin s → AffineForm e)
    (D : Set (Fin e → ℝ)) : Finset (Fin s → Fin 3) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AffineForm
theorem OAI.QuantitativeVanDerWaerden.mem_realizedSigns line 43
def OAI.QuantitativeVanDerWaerden.Arrangement.linearValue line 51
theorem OAI.QuantitativeVanDerWaerden.Arrangement.linearValue_smul line 53
theorem OAI.QuantitativeVanDerWaerden.Arrangement.linearValue_sum line 57
theorem OAI.QuantitativeVanDerWaerden.Arrangement.linearValue_neg line 63
def OAI.QuantitativeVanDerWaerden.Arrangement.thresholdFamily line 72
Source documentation
All strict homogeneous threshold supports of the fixed coefficient vectors.
```
def thresholdFamily (v : ι → Fin d → ℝ) : Finset (Finset ι) := by
…
```
theorem OAI.QuantitativeVanDerWaerden.Arrangement.mem_thresholdFamily line 76
theorem OAI.QuantitativeVanDerWaerden.Arrangement.separates_coefficients line 83
Source documentation
Shattering realizes the positive support of any coefficients on the set.
```
private theorem separates_coefficients (v : ι → Fin d → ℝ) (s : Finset ι)
    (hs : (thresholdFamily v).Shatters s) (c : s → ℝ) :
    ∃ x : Fin d → ℝ, ∀ i : s, 0 < linearValue (v i) x ↔ 0 < c i := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Arrangement.thresholdFamily, OAI.QuantitativeVanDerWaerden.Arrangement.linearValue
theorem OAI.QuantitativeVanDerWaerden.Arrangement.coefficients_nonpos line 100
Source documentation
A vanishing linear combination has no positive coefficient: choose its own positive support, making every scalar product nonnegative.
```
private theorem coefficients_nonpos (v : ι → Fin d → ℝ) (s : Finset ι)
    (hs : (thresholdFamily v).Shatters s) (c : s → ℝ)
    (hc : ∑ i : s, c i • v i = 0) : ∀ i, c i ≤ 0 := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Arrangement.thresholdFamily
theorem OAI.QuantitativeVanDerWaerden.Arrangement.shatters_linearIndependent line 127
Source documentation
Every shattered coefficient subfamily is genuinely linearly independent.
```
theorem shatters_linearIndependent (v : ι → Fin d → ℝ) (s : Finset ι)
    (hs : (thresholdFamily v).Shatters s) :
    LinearIndependent ℝ (fun i : s => v i) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Arrangement.thresholdFamily
theorem OAI.QuantitativeVanDerWaerden.Arrangement.shatters_card_le line 139
theorem OAI.QuantitativeVanDerWaerden.Arrangement.thresholdFamily_vcDim_le line 144
theorem OAI.QuantitativeVanDerWaerden.Arrangement.card_thresholdFamily_le line 153
Source documentation
Sauer--Shelah, with the dimension premise proved above, gives a uniform polynomial bound for all strict homogeneous supports.
```
theorem card_thresholdFamily_le (v : ι → Fin d → ℝ) :
    (thresholdFamily v).card ≤ (d + 1) * (Fintype.card ι + 1) ^ d := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Arrangement.thresholdFamily
def OAI.QuantitativeVanDerWaerden.Arrangement.liftedCoefficients line 180
Source documentation
The constant coefficient is the first coordinate of the homogeneous lift.
```
def liftedCoefficients {e : ℕ} (f : AffineForm e) : Fin (e + 1) → ℝ :=
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AffineForm
def OAI.QuantitativeVanDerWaerden.Arrangement.liftedPoint line 183
theorem OAI.QuantitativeVanDerWaerden.Arrangement.linearValue_lift line 185
def OAI.QuantitativeVanDerWaerden.Arrangement.signEncoding line 190
theorem OAI.QuantitativeVanDerWaerden.Arrangement.fin_three_ext line 193
theorem OAI.QuantitativeVanDerWaerden.Arrangement.signEncoding_injective line 197
theorem OAI.QuantitativeVanDerWaerden.Arrangement.signVector_encoding_mem line 206
theorem OAI.QuantitativeVanDerWaerden.card_realizedSigns_le line 225
Source documentation
Polynomial arrangement bound, including zero signs and arbitrary restrictions of the parameter domain. Its degree is independent of s.
```
theorem card_realizedSigns_le {e s : ℕ} (forms : Fin s → AffineForm e)
    (D : Set (Fin e → ℝ)) :
    (realizedSigns forms D).card ≤ (e + 2) ^ 2 * (s + 1) ^ (2 * (e + 1)) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AffineForm, OAI.QuantitativeVanDerWaerden.realizedSigns