LowDegreeInfluence.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.sum_mul_sqrt_le line 12

Source documentation

Summing pivotal-event three-halves powers using a uniform influence bound.

theorem sum_mul_sqrt_le {ι : Type u} [Fintype ι] (a : ι → ℝ) (B : ℝ)
    (ha : ∀ i, 0 ≤ a i) (hB : ∀ i, a i ≤ B) :
    (∑ i, a i * Real.sqrt (a i)) ≤ Real.sqrt B * ∑ i, a i := by
…

theorem OAI.Problem313.rpow_three_halves_eq_mul_sqrt line 22
Source documentation
A convenient conversion between real three-halves powers and square roots.
```
theorem rpow_three_halves_eq_mul_sqrt (x : ℝ) (hx : 0 ≤ x) :
    x ^ (3/2 : ℝ) = x * Real.sqrt x := by
…
```
theorem OAI.Problem313.sqrt_influence_ratio_le line 29
Source documentation
The small-total-influence regime turns the individual influence bound into a power of m.
```
theorem sqrt_influence_ratio_le (m I : ℝ) (hm : 0 < m)
    (hI : I ≤ m ^ (1/4 : ℝ)) :
    Real.sqrt (I/m) ≤ m ^ (-3/8 : ℝ) := by
…
```

theorem OAI.Problem313.low_degree_influence_bound line 45

Source documentation

The numerical case split at the end of the low-degree Fourier estimate. The factor A can be instantiated with σ².

theorem low_degree_influence_bound {ι : Type u} [Fintype ι]
    (a : ι → ℝ) (m I A L : ℝ)
    (hm : 1 ≤ m) (ha : ∀ i, 0 ≤ a i)
    (hsum : ∑ i, a i = I) (hindividual : ∀ i, a i ≤ I/m)
    (hA0 : 0 ≤ A) (hA1 : A ≤ 1)
    (hL1 : L ≤ 1)
    (hprojection : L ≤ A * m ^ (1/16 : ℝ) * ∑ i, (a i) ^ (3/2 : ℝ)) :
    L ≤ m ^ (-1/4 : ℝ) * I := by
…

theorem OAI.Problem313.low_degree_influence_bound_of_factor line 92

Source documentation

Version accepting the hypercontractive factor before its power bound is substituted.

theorem low_degree_influence_bound_of_factor {ι : Type u} [Fintype ι]
    (a : ι → ℝ) (m I A R L : ℝ)
    (hm : 1 ≤ m) (ha : ∀ i, 0 ≤ a i)
    (hsum : ∑ i, a i = I) (hindividual : ∀ i, a i ≤ I/m)
    (hA0 : 0 ≤ A) (hA1 : A ≤ 1)
    (hR : R ≤ m ^ (1/16 : ℝ)) (hL1 : L ≤ 1)
    (hprojection : L ≤ A * R * ∑ i, (a i) ^ (3/2 : ℝ)) :
    L ≤ m ^ (-1/4 : ℝ) * I := by
…