HypercontractiveTensor.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.weighted_cauchy_schwarz_sq line 12

Source documentation

Weighted Cauchy--Schwarz in a form useful for finite product measures.

theorem weighted_cauchy_schwarz_sq {α : Type u} (s : Finset α)
    (w u v : α → ℝ) (hw : ∀ x ∈ s, 0 ≤ w x) :
    (∑ x ∈ s, w x * u x * v x) ^ 2 ≤
      (∑ x ∈ s, w x * (u x) ^ 2) * (∑ x ∈ s, w x * (v x) ^ 2) := by
…

theorem OAI.Problem313.weighted_fourth_moment_add_sq line 25

Source documentation

The root-free Minkowski step in tensorization of the fourth moment.

theorem weighted_fourth_moment_add_sq {α : Type u} (s : Finset α)
    (w A B : α → ℝ) (a b : ℝ) (hw : ∀ x ∈ s, 0 ≤ w x)
    (ha : 0 ≤ a) (hb : 0 ≤ b)
    (hA : (∑ x ∈ s, w x * (A x) ^ 4) ≤ a ^ 2)
    (hB : (∑ x ∈ s, w x * (B x) ^ 4) ≤ b ^ 2) :
    (∑ x ∈ s, w x * ((A x) ^ 2 + (B x) ^ 2) ^ 2) ≤ (a + b) ^ 2 := by
…

theorem OAI.Problem313.weighted_fourth_moment_combo line 55

Source documentation

A version of the fourth-moment Minkowski step with two nonnegative coefficients.

theorem weighted_fourth_moment_combo {α : Type u} (s : Finset α)
    (w A B : α → ℝ) (a b c d : ℝ) (hw : ∀ x ∈ s, 0 ≤ w x)
    (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hd : 0 ≤ d)
    (hA : (∑ x ∈ s, w x * (A x) ^ 4) ≤ a ^ 2)
    (hB : (∑ x ∈ s, w x * (B x) ^ 4) ≤ b ^ 2) :
    (∑ x ∈ s, w x * (c * (A x) ^ 2 + d * (B x) ^ 2) ^ 2) ≤
      (c * a + d * b) ^ 2 := by
…

theorem OAI.Problem313.fourth_moment_tensor_bool line 91

Source documentation

A fourth-moment contraction tensorizes with a two-point contraction. No linearity assumptions are needed for this analytic step.

theorem fourth_moment_tensor_bool {α : Type u} [Fintype α]
    (w : α → ℝ) (q : Bool → ℝ)
    (T : (α → ℝ) → α → ℝ) (S : (Bool → ℝ) → Bool → ℝ)
    (hw : ∀ x, 0 ≤ w x) (hq : ∀ b, 0 ≤ q b)
    (hT : ∀ g, (∑ x, w x * (T g x) ^ 4) ≤ (∑ x, w x * (g x) ^ 2) ^ 2)
    (hS : ∀ g, (∑ b, q b * (S g b) ^ 4) ≤ (∑ b, q b * (g b) ^ 2) ^ 2)
    (g : Bool → α → ℝ) :
    (∑ x, ∑ b, w x * q b * (S (fun c => T (g c) x) b) ^ 4) ≤
      (∑ b, ∑ x, q b * w x * (g b x) ^ 2) ^ 2 := by
…