theorem FABL.uniformLpNormENNReal_coe.{u_1}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  (q : NNReal) (f : Ω → ℝ) :
  FABL.uniformLpNormENNReal (↑q) f =
    FABL.uniformLpNorm (↑q) f

theorem FABL.uniformLpNorm_const_mul.{u_1}
  {Ω : Type u_1} [Fintype Ω] (p c : ℝ)
  (f : Ω → ℝ) (hp : 0 < p) :
  (FABL.uniformLpNorm p fun x =>
      c * f x) =
    |c| * FABL.uniformLpNorm p f

theorem FABL.uniformLInfinityNorm_const_mul.{u_1}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  (c : ℝ) (f : Ω → ℝ) :
  (FABL.uniformLInfinityNorm fun x =>
      c * f x) =
    |c| * FABL.uniformLInfinityNorm f

theorem FABL.uniformLpNormENNReal_const_mul.{u_1}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  (q : ENNReal) (c : ℝ) (f : Ω → ℝ)
  (hq : q ≠ 0) :
  (FABL.uniformLpNormENNReal q fun x =>
      c * f x) =
    |c| * FABL.uniformLpNormENNReal q f

theorem FABL.IsHypercontractiveRandomVariable.of_normalized.{u_1}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {p q : ENNReal} (hp : p ≠ 0)
  (hq : q ≠ 0) {ρ : ℝ} {X : Ω → ℝ}
  (h :
    ∀ (a b : ℝ),
      a = 1 ∨ b = 1 →
        (FABL.uniformLpNormENNReal q
            fun x => a + ρ * b * X x) ≤
          FABL.uniformLpNormENNReal p
            fun x => a + b * X x) :
  FABL.IsHypercontractiveRandomVariable p
    q ρ X

theorem FABL.oneBit_twoSix (a b ρ : ℝ)
  (hρ : ρ ^ 2 ≤ 1 / 5) :
  (FABL.uniformLpNorm 6 fun x =>
      a + ρ * b * FABL.signValue x) ≤
    FABL.uniformLpNorm 2 fun x =>
      a + b * FABL.signValue x

theorem FABL.oneBit_twoSix_necessary_sq (ρ : ℝ)
  (h :
    ∀ (a b : ℝ),
      (FABL.uniformLpNorm 6 fun x =>
          a + ρ * b * FABL.signValue x) ≤
        FABL.uniformLpNorm 2 fun x =>
          a + b * FABL.signValue x) :
  ρ ^ 2 ≤ 1 / 5

theorem FABL.oneBit_twoSix_iff (ρ : ℝ)
  (hρ : 0 ≤ ρ) :
  (∀ (a b : ℝ),
      (FABL.uniformLpNorm 6 fun x =>
          a + ρ * b * FABL.signValue x) ≤
        FABL.uniformLpNorm 2 fun x =>
          a + b * FABL.signValue x) ↔
    ρ ≤ FABL.twoSixNoiseRoot

theorem FABL.uniformSign_twoSixHypercontractive :
  FABL.IsHypercontractiveRandomVariable 2
    6 FABL.twoSixNoiseRoot FABL.signValue

theorem FABL.oneBit_twoQ (q a b ρ : ℝ)
  (hq : 2 < q) (hρ0 : 0 ≤ ρ)
  (hρ : ρ ≤ 1 / √(q - 1)) :
  (FABL.uniformLpNorm q fun x =>
      a + ρ * b * FABL.signValue x) ≤
    FABL.uniformLpNorm 2 fun x =>
      a + b * FABL.signValue x

theorem FABL.oneBit_twoQ_sharp (q a b : ℝ)
  (hq : 2 < q) :
  (FABL.uniformLpNorm q fun x =>
      a +
        1 / √(q - 1) * b *
          FABL.signValue x) ≤
    FABL.uniformLpNorm 2 fun x =>
      a + b * FABL.signValue x

theorem FABL.oneBit_twoTop (a b : ℝ) :
  (FABL.uniformLInfinityNorm fun x =>
      a + 0 * b * FABL.signValue x) ≤
    FABL.uniformLpNorm 2 fun x =>
      a + b * FABL.signValue x

theorem FABL.uniformSign_twoQHypercontractive
  (q : NNReal) (hq : 2 < ↑q) :
  FABL.IsHypercontractiveRandomVariable 2
    (↑q) (1 / √(↑q - 1)) FABL.signValue

theorem FABL.uniformSign_twoTopHypercontractive :
  FABL.IsHypercontractiveRandomVariable 2
    ⊤ 0 FABL.signValue

theorem FABL.normalized_pTwo_affine (p e : ℝ)
  (hp1 : 1 ≤ p) (hp2 : p ≤ 2)
  (he : |e| ≤ 1) :
  √(1 + (p - 1) * e ^ 2) ≤
    (((1 + e) ^ p + (1 - e) ^ p) / 2) ^
      p⁻¹

theorem FABL.affine_pTwo_hanner (p a b : ℝ)
  (hp1 : 1 ≤ p) (hp2 : p ≤ 2) :
  √(a ^ 2 + (p - 1) * b ^ 2) ≤
    ((|a + b| ^ p + |a - b| ^ p) / 2) ^
      p⁻¹

theorem FABL.oneBit_pTwo (p a b ρ : ℝ)
  (hp1 : 1 ≤ p) (hp2 : p ≤ 2)
  (hρ0 : 0 ≤ ρ) (hρ : ρ ≤ √(p - 1)) :
  (FABL.uniformLpNorm 2 fun x =>
      a + ρ * b * FABL.signValue x) ≤
    FABL.uniformLpNorm p fun x =>
      a + b * FABL.signValue x

theorem FABL.oneBit_pTwo_sharp (p a b : ℝ)
  (hp1 : 1 ≤ p) (hp2 : p ≤ 2) :
  (FABL.uniformLpNorm 2 fun x =>
      a +
        √(p - 1) * b * FABL.signValue x) ≤
    FABL.uniformLpNorm p fun x =>
      a + b * FABL.signValue x

theorem FABL.uniformSign_pTwoHypercontractive
  (p : NNReal) (hp1 : 1 ≤ ↑p)
  (hp2 : ↑p ≤ 2) :
  FABL.IsHypercontractiveRandomVariable
    (↑p) 2 (√(↑p - 1)) FABL.signValue

theorem FABL.uniformInner_le_uniformLpNorm_mul.{u_1}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {p q : ℝ} (hpq : p.HolderConjugate q)
  (f g : Ω → ℝ) :
  FABL.uniformInner f g ≤
    FABL.uniformLpNorm p f *
      FABL.uniformLpNorm q g

theorem FABL.exists_uniformLpNorm_dual.{u_1}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  (q p : ℝ) (hpq : q.HolderConjugate p)
  (f : Ω → ℝ) :
  ∃ g,
    FABL.uniformLpNorm p g ≤ 1 ∧
      FABL.uniformInner f g =
        FABL.uniformLpNorm q f

theorem FABL.selfAdjoint_dual_bound.{u_1}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  (p q p' q' C : ℝ)
  (hp : p.HolderConjugate p')
  (hq : q.HolderConjugate q')
  (T : (Ω → ℝ) → Ω → ℝ)
  (hself :
    ∀ (f g : Ω → ℝ),
      FABL.uniformInner (T f) g =
        FABL.uniformInner f (T g))
  (hbound :
    ∀ (f : Ω → ℝ),
      FABL.uniformLpNorm q (T f) ≤
        C * FABL.uniformLpNorm p f)
  (g : Ω → ℝ) :
  FABL.uniformLpNorm p' (T g) ≤
    C * FABL.uniformLpNorm q' g