ProjectionNorm.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.weighted_holder_four_thirds line 13

Source documentation

Weighted finite Hölder inequality with conjugate exponents 4/3 and 4. Weights need not be normalized.

theorem weighted_holder_four_thirds {ι : Type u} [Fintype ι]
    (w v u : ι → ℝ) (hw : ∀ i, 0 ≤ w i) :
    |∑ i, w i * v i * u i| ≤
      (∑ i, w i * |v i| ^ (4 / 3 : ℝ)) ^ (3 / 4 : ℝ) *
        (∑ i, w i * u i ^ 4) ^ (1 / 4 : ℝ) := by
…

theorem OAI.Problem313.projection_moment_bound line 61

Source documentation

The scalar cancellation behind the L⁴ duality argument.

theorem projection_moment_bound {M V H A : ℝ}
    (hM : 0 ≤ M) (hV : 0 ≤ V) (hH : 0 ≤ H) (hA : 0 ≤ A)
    (hdual : M ≤ V ^ (3 / 4 : ℝ) * H ^ (1 / 4 : ℝ))
    (hfour : H ≤ A ^ 4 * M ^ 2) :
    M ≤ A ^ 2 * V ^ (3 / 2 : ℝ) := by
…

theorem OAI.Problem313.weighted_projection_bound line 95

Source documentation

A low-degree fourth-moment bound implies the dual projection estimate. The hypothesis hproj is the usual orthogonal-projection identity ⟨v,u⟩ = ⟨u,u⟩; this formulation avoids choosing a normalized dual vector.

theorem weighted_projection_bound {ι : Type u} [Fintype ι]
    (w v u : ι → ℝ) (hw : ∀ i, 0 ≤ w i) (A : ℝ) (hA : 0 ≤ A)
    (hproj : (∑ i, w i * v i * u i) = ∑ i, w i * u i ^ 2)
    (hfour : (∑ i, w i * u i ^ 4) ≤ A ^ 4 * (∑ i, w i * u i ^ 2) ^ 2) :
    (∑ i, w i * u i ^ 2) ≤
      A ^ 2 * (∑ i, w i * |v i| ^ (4 / 3 : ℝ)) ^ (3 / 2 : ℝ) := by
…

theorem OAI.Problem313.weighted_projection_pivotal_bound line 113

Source documentation

Dual projection estimate for functions taking their values in {-1,0,1}, as Boolean coordinate differences do.

theorem weighted_projection_pivotal_bound {ι : Type u} [Fintype ι]
    (w v u : ι → ℝ) (hw : ∀ i, 0 ≤ w i)
    (hv : ∀ i, v i = -1 ∨ v i = 0 ∨ v i = 1)
    (A : ℝ) (hA : 0 ≤ A)
    (hproj : (∑ i, w i * v i * u i) = ∑ i, w i * u i ^ 2)
    (hfour : (∑ i, w i * u i ^ 4) ≤ A ^ 4 * (∑ i, w i * u i ^ 2) ^ 2) :
    (∑ i, w i * u i ^ 2) ≤
      A ^ 2 * (∑ i, if v i ≠ 0 then w i else 0) ^ (3 / 2 : ℝ) := by
…

theorem OAI.Problem313.weighted_projection_noise_bound line 130

Source documentation

The exponent form used for low-degree projections of Boolean derivatives.

theorem weighted_projection_noise_bound {ι : Type u} [Fintype ι]
    (w v u : ι → ℝ) (hw : ∀ i, 0 ≤ w i)
    (hv : ∀ i, v i = -1 ∨ v i = 0 ∨ v i = 1)
    (ρ d : ℝ) (hρ : 0 ≤ ρ)
    (hproj : (∑ i, w i * v i * u i) = ∑ i, w i * u i ^ 2)
    (hfour : (∑ i, w i * u i ^ 4) ≤
      ρ ^ (-4 * d) * (∑ i, w i * u i ^ 2) ^ 2) :
    (∑ i, w i * u i ^ 2) ≤
      ρ ^ (-2 * d) * (∑ i, if v i ≠ 0 then w i else 0) ^ (3 / 2 : ℝ) := by
…