Source indexedlemma · leanprover/lean4:v4.32.0

rudin_exp_abs_ineq

APAP.Prereqs.Rudin · APAP/Prereqs/Rudin.lean:61 to 68

Source documentation

Rudin's inequality, exponential form with absolute values.

Exact Lean statement

lemma rudin_exp_abs_ineq (f : G → ℂ) (hf : AddDissociated <| support <| cft f) :
    𝔼 a, exp |(f a).re| ≤ 2 * exp (‖f‖ₙ_[2] ^ 2 / 2)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rudin_exp_abs_ineq (f : G → ℂ) (hf : AddDissociated <| support <| cft f) :    𝔼 a, exp |(f a).re| ≤ 2 * exp (‖f‖ₙ_[2] ^ 2 / 2) := by  calc    _ ≤ 𝔼 a, (exp (f a).re + exp (-f a).re) := expect_le_expect fun _ _ ↦ exp_abs_le _    _ = 𝔼 a, exp (f a).re + 𝔼 a, exp ((-f) a).re := by simp [expect_add_distrib]    _ ≤ exp (‖f‖ₙ_[2] ^ 2 / 2) + exp (‖-f‖ₙ_[2] ^ 2 / 2) :=        add_le_add (rudin_exp_ineq f hf) (rudin_exp_ineq (-f) <| by simpa using hf)    _ = _ := by simp [two_mul]