TwoPoint.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem313.fourth_power_centered_bound line 10
Source documentation
A pointwise fourth-power estimate with the linear term retained for averaging.
```
lemma fourth_power_centered_bound (a z : ℝ) :
    (a + z) ^ 4 ≤ a ^ 4 + 4 * a ^ 3 * z + 8 * a ^ 2 * z ^ 2 + 3 * z ^ 4 := by
…
```
theorem OAI.Problem313.biased_two_point_fourth_moment line 18
Source documentation
The scalar two-point estimate used to tensorize biased hypercontractivity. The noise parameter is sqrt (p * (1-p)) / 4; after cancellation of the normalization in the biased character, its two values are -p / 4 and (1-p) / 4. This formulation also includes the endpoint biases.
```
theorem biased_two_point_fourth_moment (p a b : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1) :
    (1 - p) * (a - p * b / 4) ^ 4 + p * (a + (1 - p) * b / 4) ^ 4 ≤
      (a ^ 2 + b ^ 2) ^ 2 := by
…
```

lemma OAI.Problem313.two_point_second_moment line 38

Source documentation

Mean and variance decomposition for a two-point law, without division.

lemma two_point_second_moment (p u v : ℝ) :
    ((1 - p) * u + p * v) ^ 2 + p * (1 - p) * (v - u) ^ 2 =
      (1 - p) * u ^ 2 + p * v ^ 2 := by
…

theorem OAI.Problem313.biased_two_point_noise_fourth line 45
Source documentation
The scalar noise contraction in raw function values. This is the (1 - ρ) * expectation + ρ * identity form, suitable for tensor products.
```
theorem biased_two_point_noise_fourth (p ρ u v : ℝ)
    (hp : 0 ≤ p) (hp1 : p ≤ 1) (hρ : 16 * ρ ^ 2 ≤ p * (1 - p)) :
    let μ := (1 - p) * u + p * v
…
```

theorem OAI.Problem313.biased_bool_noise_fourth line 66

Source documentation

Finite-sum formulation of the two-point noise contraction.

theorem biased_bool_noise_fourth (p ρ : ℝ) (f : Bool → ℝ)
    (hp : 0 ≤ p) (hp1 : p ≤ 1) (hρ : 16 * ρ ^ 2 ≤ p * (1 - p)) :
    let w : Bool → ℝ := fun b => if b = true then p else 1 - p
…