theorem exists_decomp_le_kNorm_add.{u_1}exists_decomp_le_kNorm_add.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) {δ : ℝ≥0∞} (hδ : δ ≠ 0) (x : α)
  (ν : ℤ) : ∃ y z, y + z = x ∧ ‖y‖ₑ[A.fst] + 2 ^ ν * ‖z‖ₑ[A.snd] ≤ A.kNorm (2 ^ ν) x + δLet $x \in \alpha$, $\delta > 0$ and $\nu \in \mathbb{Z}$. There is a decomposition
$x = y + z$ with $$\|y\|_0 + 2^\nu \|z\|_1 \le K_\nu(x) + \delta$$. 
  {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 αType u_1]
  (ACouple α : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 αType u_1) {δℝ≥0∞ : ℝ≥0∞ENNReal : Type} (hδδ ≠ 0 : δℝ≥0∞ ≠Ne.{u} {α : Sort u} (a b : α) : Prop 0)
  (xα : αType u_1) (νℤ : ℤInt : Type) :
  ∃ yα zα,
    yα +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ zα =Eq.{u_1} {α : Sort u_1} : α → α → Prop xα ∧And (a b : Prop) : Prop
      ‖yα‖ₑ[ACouple α.fstEQuasinorm.Couple.fst.{u_1} {α : Type u_1} [AddCommMonoid α] (self : Couple α) : EQuasinorm α] +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ 2 ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ νℤ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ ‖zα‖ₑ[ACouple α.sndEQuasinorm.Couple.snd.{u_1} {α : Type u_1} [AddCommMonoid α] (self : Couple α) : EQuasinorm α] ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop
        ACouple α.kNormEQuasinorm.Couple.kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞ (HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ2 ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ νℤ)HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ xα +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ δℝ≥0∞

theorem exists_seq_decomp_le_kNorm_add.{u_1}exists_seq_decomp_le_kNorm_add.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) {δ : ℝ≥0∞} (hδ : δ ≠ 0) (x : α) :
  ∃ y z, ∀ (ν : ℤ), y ν + z ν = x ∧ ‖y ν‖ₑ[A.fst] + 2 ^ ν * ‖z ν‖ₑ[A.snd] ≤ A.kNorm (2 ^ ν) x + δLet $x \in \alpha$ and $\delta > 0$. There are sequences $(y_\nu)$, $(z_\nu)$ with
$x = y_\nu + z_\nu$ and $$\|y_\nu\|_0 + 2^\nu \|z_\nu\|_1 \le K_\nu(x) + \delta$$ for all
$\nu \in \mathbb{Z}$. 
  {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 αType u_1]
  (ACouple α : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 αType u_1) {δℝ≥0∞ : ℝ≥0∞ENNReal : Type} (hδδ ≠ 0 : δℝ≥0∞ ≠Ne.{u} {α : Sort u} (a b : α) : Prop 0)
  (xα : αType u_1) :
  ∃ yℤ → α zℤ → α,
    ∀ (νℤ : ℤInt : Type),
      yℤ → α νℤ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ zℤ → α νℤ =Eq.{u_1} {α : Sort u_1} : α → α → Prop xα ∧And (a b : Prop) : Prop
        ‖yℤ → α νℤ‖ₑ[ACouple α.fstEQuasinorm.Couple.fst.{u_1} {α : Type u_1} [AddCommMonoid α] (self : Couple α) : EQuasinorm α] +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ
            2 ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ νℤ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ ‖zℤ → α νℤ‖ₑ[ACouple α.sndEQuasinorm.Couple.snd.{u_1} {α : Type u_1} [AddCommMonoid α] (self : Couple α) : EQuasinorm α] ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop
          ACouple α.kNormEQuasinorm.Couple.kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞ (HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ2 ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ νℤ)HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ xα +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ δℝ≥0∞

theorem jInfNorm_le_discretePhiFunctional.{u_1}jInfNorm_le_discretePhiFunctional.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) {θ : ℝ} {q : ℝ≥0∞} {x : α}
  {a : ℤ → α} (ha : (Function.support a).Finite) (hsum : ∑ᶠ (n : ℤ), a n = x) :
  jInfNorm A θ q x ≤ discretePhiFunctional θ q fun n ↦ A.jNorm (2 ^ n) (a n)A finitely supported $a \colon \mathbb{Z} \to \alpha$ with $\sum_n a_n = x$ bounds
`jInfNorm` by its cost. 
  {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 αType u_1]
  (ACouple α : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 αType u_1) {θℝ : ℝReal : Type} {qℝ≥0∞ : ℝ≥0∞ENNReal : Type}
  {xα : αType u_1} {aℤ → α : ℤInt : Type → αType u_1}
  (ha(Function.support a).Finite : (Function.supportFunction.support.{u_1, u_3} {ι : Type u_1} {M : Type u_3} [Zero M] (f : ι → M) : Set ι aℤ → α).FiniteSet.Finite.{u} {α : Type u} (s : Set α) : Prop)
  (hsum∑ᶠ (n : ℤ), a n = x : ∑ᶠfinsum.{u_6, u_7} {M : Type u_6} {α : Sort u_7} [AddCommMonoid M] (f : α → M) : M (nℤ : ℤInt : Type),finsum.{u_6, u_7} {M : Type u_6} {α : Sort u_7} [AddCommMonoid M] (f : α → M) : M aℤ → α nℤ =Eq.{u_1} {α : Sort u_1} : α → α → Prop xα) :
  jInfNormjInfNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) (x : α) : ℝ≥0∞The norm
$$\inf\Bigl\{\,\bigl\|\{2^{-\theta n}J(2^{n},a_{n})\}_{n \in \mathbb{Z}}\bigr\|_{\ell^{q}}
 : a \colon \mathbb{Z} \to \alpha \text{ finitely supported},\ \sum_{n}a_{n}=x\,\Bigr\}.$$  ACouple α θℝ qℝ≥0∞ xα ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop
    discretePhiFunctionalEQuasinorm.discretePhiFunctional (θ : ℝ) (q : ℝ≥0∞) (f : ℤ → ℝ≥0∞) : ℝ≥0∞ θℝ qℝ≥0∞ fun nℤ ↦
      ACouple α.jNormEQuasinorm.Couple.jNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞ (HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ2 ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ nℤ)HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ (aℤ → α nℤ)

theorem jInfNorm_exponent_zero.{u_1}jInfNorm_exponent_zero.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (x : α) : jInfNorm A θ 0 x = 0For $q = 0$, `jInfNorm` vanishes: the family equal to $x$ at $0$ and to $0$
elsewhere costs $0$. 
  {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 αType u_1]
  (ACouple α : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 αType u_1) (θℝ : ℝReal : Type) (xα : αType u_1) :
  jInfNormjInfNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) (x : α) : ℝ≥0∞The norm
$$\inf\Bigl\{\,\bigl\|\{2^{-\theta n}J(2^{n},a_{n})\}_{n \in \mathbb{Z}}\bigr\|_{\ell^{q}}
 : a \colon \mathbb{Z} \to \alpha \text{ finitely supported},\ \sum_{n}a_{n}=x\,\Bigr\}.$$  ACouple α θℝ 0 xα =Eq.{u_1} {α : Sort u_1} : α → α → Prop 0

theorem jInfNorm_swap.{u_1}jInfNorm_swap.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) (x : α) :
  jInfNorm A.swap θ q x = jInfNorm A (1 - θ) q xSwapping the two quasinorms replaces $θ$ by $1 - θ$ in `jInfNorm`.  {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 αType u_1] (ACouple α : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 αType u_1) (θℝ : ℝReal : Type)
  (qℝ≥0∞ : ℝ≥0∞ENNReal : Type) (xα : αType u_1) :
  jInfNormjInfNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) (x : α) : ℝ≥0∞The norm
$$\inf\Bigl\{\,\bigl\|\{2^{-\theta n}J(2^{n},a_{n})\}_{n \in \mathbb{Z}}\bigr\|_{\ell^{q}}
 : a \colon \mathbb{Z} \to \alpha \text{ finitely supported},\ \sum_{n}a_{n}=x\,\Bigr\}.$$  ACouple α.swapEQuasinorm.Couple.swap.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) : Couple α θℝ qℝ≥0∞ xα =Eq.{u_1} {α : Sort u_1} : α → α → Prop
    jInfNormjInfNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) (x : α) : ℝ≥0∞The norm
$$\inf\Bigl\{\,\bigl\|\{2^{-\theta n}J(2^{n},a_{n})\}_{n \in \mathbb{Z}}\bigr\|_{\ell^{q}}
 : a \colon \mathbb{Z} \to \alpha \text{ finitely supported},\ \sum_{n}a_{n}=x\,\Bigr\}.$$  ACouple α (HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ1 -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ θℝ)HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ qℝ≥0∞ xα

theorem exists_decomp_Icc.{u_1, u_2}exists_decomp_Icc.{u_1, u_2} {α : Type u_1} [AddCommMonoid α] {M : Type u_2} [AddCommMonoid M] [Preorder M]
  [Modulus α M] [Modulus.IsDecomposable α M] {x : α} {y z : ℤ → α} (hyz : ∀ (μ : ℤ), y μ + z μ = x) (a : ℤ) (m : ℕ)
  {r : α} (hr : |r|ₑ ≤ |x|ₑ) :
  ∃ u,
    Function.support u ⊆ ↑(Finset.Icc a (a + ↑m)) ∧
      ∑ᶠ (ν : ℤ), u ν = r ∧ ∀ (ν : ℤ), |u ν|ₑ ≤ |r|ₑ ∧ (ν < a + ↑m → |u ν|ₑ ≤ |y (ν + 1)|ₑ) ∧ (a < ν → |u ν|ₑ ≤ |z ν|ₑ)Let $x = y_\mu + z_\mu$ for all $\mu \in \mathbb{Z}$, let $a \in \mathbb{Z}$, $m \in \mathbb{N}$
and $r \in \alpha$ with $|r| \le |x|$, and put $I = \{a, \dots, a+m\}$. Then there is
$u \colon \mathbb{Z} \to \alpha$ vanishing outside $I$ with
$\sum_{\nu \in \mathbb{Z}} u_\nu = r$ and,
for $\nu \in I$:

* $|u_\nu| \le |y_{\nu+1}|$ if $\nu < a + m$;

* $|u_\nu| \le |z_\nu|$ if $a < \nu$;

* $|u_\nu| \le |r|$.

  {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 αType u_1]
  {MType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 MType u_2]
  [PreorderPreorder.{u_2} (α : Type u_2) : Type u_2 MType u_2] [ModulusModulus.{u_3, u_4} (β : Type u_3) (M : outParam (Type u_4)) : Type (max u_3 u_4) αType u_1 MType u_2]
  [Modulus.IsDecomposableModulus.IsDecomposable.{u_1, u_3} (β : Type u_1) [AddCommMonoid β] (M : outParam (Type u_3)) [AddCommMonoid M]
  [Preorder M] [Modulus β M] : Prop αType u_1 MType u_2] {xα : αType u_1}
  {yℤ → α zℤ → α : ℤInt : Type → αType u_1}
  (hyz∀ (μ : ℤ), y μ + z μ = x : ∀ (μℤ : ℤInt : Type), yℤ → α μℤ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ zℤ → α μℤ =Eq.{u_1} {α : Sort u_1} : α → α → Prop xα) (aℤ : ℤInt : Type)
  (mℕ : ℕNat : Type) {rα : αType u_1} (hr|r|ₑ ≤ |x|ₑ : |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Mrα|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Mxα|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M) :
  ∃ uℤ → α,
    Function.supportFunction.support.{u_1, u_3} {ι : Type u_1} {M : Type u_3} [Zero M] (f : ι → M) : Set ι uℤ → α ⊆
        ↑(Finset.IccFinset.Icc.{u_1} {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Finset α aℤ (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γaℤ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ ↑mℕ)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ) ∧And (a b : Prop) : Prop
      ∑ᶠfinsum.{u_6, u_7} {M : Type u_6} {α : Sort u_7} [AddCommMonoid M] (f : α → M) : M (νℤ : ℤInt : Type),finsum.{u_6, u_7} {M : Type u_6} {α : Sort u_7} [AddCommMonoid M] (f : α → M) : M uℤ → α νℤ =Eq.{u_1} {α : Sort u_1} : α → α → Prop rα ∧And (a b : Prop) : Prop
        ∀ (νℤ : ℤInt : Type),
          |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Muℤ → α νℤ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Mrα|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M ∧And (a b : Prop) : Prop
            (νℤ <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop aℤ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ ↑mℕ →
                |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Muℤ → α νℤ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Myℤ → α (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γνℤ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ 1)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M) ∧And (a b : Prop) : Prop
              (aℤ <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop νℤ → |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Muℤ → α νℤ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Mzℤ → α νℤ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M)

theorem exists_decomp_Ico_symm.{u_1, u_2}exists_decomp_Ico_symm.{u_1, u_2} {α : Type u_1} [AddCommMonoid α] {M : Type u_2} [AddCommMonoid M] [Preorder M]
  [Modulus α M] [Modulus.IsDecomposable α M] {x : α} {y z : ℤ → α} (hyz : ∀ (μ : ℤ), y μ + z μ = x) {N : ℕ}
  (hN : 1 ≤ N) :
  ∃ u,
    Function.support u ⊆ ↑(Finset.Ico (-↑N) ↑N) ∧
      ∑ᶠ (ν : ℤ), u ν = x ∧
        ∀ (ν : ℤ), |u ν|ₑ ≤ |x|ₑ ∧ (ν < ↑N - 1 → |u ν|ₑ ≤ |y (ν + 1)|ₑ) ∧ (-↑N < ν → |u ν|ₑ ≤ |z ν|ₑ)Let $N \ge 1$ and $x = y_\mu + z_\mu$ for all $\mu \in \mathbb{Z}$. Then there is
$u \colon \mathbb{Z} \to \alpha$ vanishing outside $\{-N, \dots, N-1\}$ with
$\sum_{\nu \in \mathbb{Z}} u_\nu = x$ and:

* $|u_\nu| \le |y_{\nu+1}|$ if $\nu < N - 1$;

* $|u_\nu| \le |z_\nu|$ if $-N < \nu$;

* $|u_\nu| \le |x|$.

  {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 αType u_1]
  {MType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 MType u_2]
  [PreorderPreorder.{u_2} (α : Type u_2) : Type u_2 MType u_2] [ModulusModulus.{u_3, u_4} (β : Type u_3) (M : outParam (Type u_4)) : Type (max u_3 u_4) αType u_1 MType u_2]
  [Modulus.IsDecomposableModulus.IsDecomposable.{u_1, u_3} (β : Type u_1) [AddCommMonoid β] (M : outParam (Type u_3)) [AddCommMonoid M]
  [Preorder M] [Modulus β M] : Prop αType u_1 MType u_2] {xα : αType u_1}
  {yℤ → α zℤ → α : ℤInt : Type → αType u_1}
  (hyz∀ (μ : ℤ), y μ + z μ = x : ∀ (μℤ : ℤInt : Type), yℤ → α μℤ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ zℤ → α μℤ =Eq.{u_1} {α : Sort u_1} : α → α → Prop xα) {Nℕ : ℕNat : Type}
  (hN1 ≤ N : 1 ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop Nℕ) :
  ∃ uℤ → α,
    Function.supportFunction.support.{u_1, u_3} {ι : Type u_1} {M : Type u_3} [Zero M] (f : ι → M) : Set ι uℤ → α ⊆
        ↑(Finset.IcoFinset.Ico.{u_1} {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Finset α (Neg.neg.{u} {α : Type u} [self : Neg α] : α → α-Neg.neg.{u} {α : Type u} [self : Neg α] : α → α↑Nℕ)Neg.neg.{u} {α : Type u} [self : Neg α] : α → α ↑Nℕ) ∧And (a b : Prop) : Prop
      ∑ᶠfinsum.{u_6, u_7} {M : Type u_6} {α : Sort u_7} [AddCommMonoid M] (f : α → M) : M (νℤ : ℤInt : Type),finsum.{u_6, u_7} {M : Type u_6} {α : Sort u_7} [AddCommMonoid M] (f : α → M) : M uℤ → α νℤ =Eq.{u_1} {α : Sort u_1} : α → α → Prop xα ∧And (a b : Prop) : Prop
        ∀ (νℤ : ℤInt : Type),
          |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Muℤ → α νℤ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Mxα|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M ∧And (a b : Prop) : Prop
            (νℤ <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop ↑Nℕ -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ 1 →
                |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Muℤ → α νℤ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Myℤ → α (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γνℤ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ 1)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M) ∧And (a b : Prop) : Prop
              (-Neg.neg.{u} {α : Type u} [self : Neg α] : α → α↑Nℕ <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop νℤ → |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Muℤ → α νℤ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Mzℤ → α νℤ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M)

theorem tendsto_discretePhiFunctional_boundaryError_rpow.{u_1}tendsto_discretePhiFunctional_boundaryError_rpow.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) {θ : ℝ}
  (hθ : θ ∈ Ioo 0 1) {q : ℝ≥0∞} (hq : q ≠ 0) {x : α} (hx : x ∈ A.inf.finiteLocus) :
  Tendsto (fun N ↦ discretePhiFunctional θ q (boundaryError A N x) ^ (min q 1).toReal) atTop (𝓝 0)For $0 < θ < 1$, $q ≠ 0$ and $x ∈ A_0 ∩ A_1$, with $r = \min(q, 1)$,
$Φ_{θ,q}(E_N)^r → 0$ as $N → ∞$. The two terms of $E_N$ contribute
$2^{(θ-1)N}\|x\|_1$ and $2^θ\,2^{-θN}\|x\|_0$ to $Φ_{θ,q}$. 
  {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 αType u_1]
  (ACouple α : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 αType u_1) {θℝ : ℝReal : Type}
  (hθθ ∈ Ioo 0 1 : θℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → Prop IooSet.Ioo.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α 0 1) {qℝ≥0∞ : ℝ≥0∞ENNReal : Type}
  (hqq ≠ 0 : qℝ≥0∞ ≠Ne.{u} {α : Sort u} (a b : α) : Prop 0) {xα : αType u_1}
  (hxx ∈ A.inf.finiteLocus : xα ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → Prop ACouple α.infEQuasinorm.Couple.inf.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) : EQuasinorm α.finiteLocusEQuasinorm.finiteLocus.{u_1} {α : Type u_1} [AddCommMonoid α] (A : EQuasinorm α) : AddSubmonoid α) :
  TendstoFilter.Tendsto.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) (l₁ : Filter α) (l₂ : Filter β) : Prop
    (fun Nℕ ↦
      discretePhiFunctionalEQuasinorm.discretePhiFunctional (θ : ℝ) (q : ℝ≥0∞) (f : ℤ → ℝ≥0∞) : ℝ≥0∞ θℝ qℝ≥0∞
          (boundaryErrorboundaryError.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (N : ℕ) (x : α) : ℤ → ℝ≥0∞The error at the two ends of the decomposition of `exists_decomp_Ico_symm`:
$$E_N = 2^{-N}\|x\|_1\,\mathbf{1}_{\{-N\}} + \|x\|_0\,\mathbf{1}_{\{N-1\}}.$$  ACouple α Nℕ xα) ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ
        (minMin.min.{u} {α : Type u} [self : Min α] : α → α → α qℝ≥0∞ 1).toRealENNReal.toReal (a : ℝ≥0∞) : ℝ)
    atTopFilter.atTop.{u_2} {α : Type u_2} [Preorder α] : Filter α (𝓝nhds.{u_3} {X : Type u_3} [TopologicalSpace X] (x : X) : Filter X 0)

theorem jNorm_le_kNorm_add.{u_1, u_2}jNorm_le_kNorm_add.{u_1, u_2} {α : Type u_1} [AddCommMonoid α] (A : Couple α) {M : Type u_2} [Preorder M] [Modulus α M]
  [A.fst.IsSolid] [A.snd.IsSolid] {x : α} {y z u : ℤ → α} {δ : ℝ≥0∞} {N : ℕ}
  (hyz : ∀ (μ : ℤ), ‖y μ‖ₑ[A.fst] + 2 ^ μ * ‖z μ‖ₑ[A.snd] ≤ A.kNorm (2 ^ μ) x + δ)
  (hsupp : Function.support u ⊆ Ico (-↑N) ↑N)
  (hu : ∀ (ν : ℤ), |u ν|ₑ ≤ |x|ₑ ∧ (ν < ↑N - 1 → |u ν|ₑ ≤ |y (ν + 1)|ₑ) ∧ (-↑N < ν → |u ν|ₑ ≤ |z ν|ₑ)) (ν : ℤ) :
  A.jNorm (2 ^ ν) (u ν) ≤ A.kNorm (2 ^ (ν + 1)) x + (Ico (-↑N) ↑N).indicator (fun x ↦ δ) ν + boundaryError A N x νLet $\|y_\mu\|_0 + 2^\mu \|z_\mu\|_1 \le K_\mu(x) + \delta$ for all $\mu \in \mathbb{Z}$,
and let $u$ vanish outside $\{-N, \dots, N-1\}$ and satisfy the bounds of
`exists_decomp_Ico_symm`. Then for every $\nu \in \mathbb{Z}$, with $E_N$ the
`boundaryError`,
$$J_\nu(u_\nu) \le K_{\nu+1}(x) + \delta\,\mathbf{1}_{\{-N,\dots,N-1\}}(\nu) + E_N(\nu).$$
For $-N \le \nu \le N-1$, solidity gives $\|u_\nu\|_0 \le \|y_{\nu+1}\|_0$ and
$2^\nu\|u_\nu\|_1 \le 2^\nu\|z_\nu\|_1$, both at most $K_{\nu+1}(x) + \delta$, except at
$\nu = N-1$ and at $\nu = -N$ respectively, where only $|u_\nu| \le |x|$ is available.

  {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 αType u_1]
  (ACouple α : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 αType u_1) {MType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [PreorderPreorder.{u_2} (α : Type u_2) : Type u_2 MType u_2] [ModulusModulus.{u_3, u_4} (β : Type u_3) (M : outParam (Type u_4)) : Type (max u_3 u_4) αType u_1 MType u_2]
  [ACouple α.fstEQuasinorm.Couple.fst.{u_1} {α : Type u_1} [AddCommMonoid α] (self : Couple α) : EQuasinorm α.IsSolidEQuasinorm.IsSolid.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [Preorder M] [Modulus β M]
  (B : EQuasinorm β) : Prop] [ACouple α.sndEQuasinorm.Couple.snd.{u_1} {α : Type u_1} [AddCommMonoid α] (self : Couple α) : EQuasinorm α.IsSolidEQuasinorm.IsSolid.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [Preorder M] [Modulus β M]
  (B : EQuasinorm β) : Prop] {xα : αType u_1}
  {yℤ → α zℤ → α uℤ → α : ℤInt : Type → αType u_1} {δℝ≥0∞ : ℝ≥0∞ENNReal : Type} {Nℕ : ℕNat : Type}
  (hyz∀ (μ : ℤ), ‖y μ‖ₑ[A.fst] + 2 ^ μ * ‖z μ‖ₑ[A.snd] ≤ A.kNorm (2 ^ μ) x + δ :
    ∀ (μℤ : ℤInt : Type),
      ‖yℤ → α μℤ‖ₑ[ACouple α.fstEQuasinorm.Couple.fst.{u_1} {α : Type u_1} [AddCommMonoid α] (self : Couple α) : EQuasinorm α] +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ
          2 ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ μℤ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ ‖zℤ → α μℤ‖ₑ[ACouple α.sndEQuasinorm.Couple.snd.{u_1} {α : Type u_1} [AddCommMonoid α] (self : Couple α) : EQuasinorm α] ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop
        ACouple α.kNormEQuasinorm.Couple.kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞ (HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ2 ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ μℤ)HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ xα +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ δℝ≥0∞)
  (hsuppFunction.support u ⊆ Ico (-↑N) ↑N :
    Function.supportFunction.support.{u_1, u_3} {ι : Type u_1} {M : Type u_3} [Zero M] (f : ι → M) : Set ι uℤ → α ⊆ IcoSet.Ico.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α (Neg.neg.{u} {α : Type u} [self : Neg α] : α → α-Neg.neg.{u} {α : Type u} [self : Neg α] : α → α↑Nℕ)Neg.neg.{u} {α : Type u} [self : Neg α] : α → α ↑Nℕ)
  (hu∀ (ν : ℤ), |u ν|ₑ ≤ |x|ₑ ∧ (ν < ↑N - 1 → |u ν|ₑ ≤ |y (ν + 1)|ₑ) ∧ (-↑N < ν → |u ν|ₑ ≤ |z ν|ₑ) :
    ∀ (νℤ : ℤInt : Type),
      |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Muℤ → α νℤ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Mxα|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M ∧And (a b : Prop) : Prop
        (νℤ <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop ↑Nℕ -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ 1 →
            |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Muℤ → α νℤ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Myℤ → α (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γνℤ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ 1)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M) ∧And (a b : Prop) : Prop
          (-Neg.neg.{u} {α : Type u} [self : Neg α] : α → α↑Nℕ <LT.lt.{u} {α : Type u} [self : LT α] : α → α → Prop νℤ → |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Muℤ → α νℤ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop |Modulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → Mzℤ → α νℤ|ₑModulus.modulus.{u_3, u_4} {β : Type u_3} {M : outParam (Type u_4)} [self : Modulus β M] : β → M))
  (νℤ : ℤInt : Type) :
  ACouple α.jNormEQuasinorm.Couple.jNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞ (HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ2 ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ νℤ)HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ (uℤ → α νℤ) ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop
    ACouple α.kNormEQuasinorm.Couple.kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞ (HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ2 ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γνℤ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ 1)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ)HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ xα +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ
        (IcoSet.Ico.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α (Neg.neg.{u} {α : Type u} [self : Neg α] : α → α-Neg.neg.{u} {α : Type u} [self : Neg α] : α → α↑Nℕ)Neg.neg.{u} {α : Type u} [self : Neg α] : α → α ↑Nℕ).indicatorSet.indicator.{u_1, u_3} {α : Type u_1} {M : Type u_3} [Zero M] (s : Set α) (f : α → M) (x : α) : M
          (fun xℤ ↦ δℝ≥0∞) νℤ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ
      boundaryErrorboundaryError.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (N : ℕ) (x : α) : ℤ → ℝ≥0∞The error at the two ends of the decomposition of `exists_decomp_Ico_symm`:
$$E_N = 2^{-N}\|x\|_1\,\mathbf{1}_{\{-N\}} + \|x\|_0\,\mathbf{1}_{\{N-1\}}.$$  ACouple α Nℕ xα νℤ

theorem jInfNorm_le_discretePhiFunctional_kNorm_add.{u_1,
    u_2}jInfNorm_le_discretePhiFunctional_kNorm_add.{u_1, u_2} {α : Type u_1} [AddCommMonoid α] (A : Couple α) {M : Type u_2}
  [AddCommMonoid M] [Preorder M] [Modulus α M] [Modulus.IsDecomposable α M] [A.fst.IsSolid] [A.snd.IsSolid] (θ : ℝ)
  (q : ℝ≥0∞) {δ : ℝ≥0∞} (hδ : δ ≠ 0) {N : ℕ} (hN : 1 ≤ N) (x : α) :
  jInfNorm A θ q x ≤
    discretePhiFunctional θ q
      (((fun ν ↦ A.kNorm (2 ^ (ν + 1)) x) + (Ico (-↑N) ↑N).indicator fun x ↦ δ) + boundaryError A N x)For $N ≥ 1$ and $δ > 0$, with $E_N$ the `boundaryError`,
$$\mathcal{J}(x) \le \Phi_{\theta,q}\bigl(\nu \mapsto K_{\nu+1}(x)
  + \delta\,\mathbf{1}_{\{-N,\dots,N-1\}}(\nu) + E_N(\nu)\bigr).$$
The family $u$ of `exists_decomp_Ico_symm` is admissible, and
`jNorm_le_kNorm_add` bounds its cost termwise.

  {αType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 αType u_1]
  (ACouple α : CoupleEQuasinorm.Couple.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 αType u_1) {MType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommMonoidAddCommMonoid.{u_2} (M : Type u_2) : Type u_2 MType u_2] [PreorderPreorder.{u_2} (α : Type u_2) : Type u_2 MType u_2]
  [ModulusModulus.{u_3, u_4} (β : Type u_3) (M : outParam (Type u_4)) : Type (max u_3 u_4) αType u_1 MType u_2]
  [Modulus.IsDecomposableModulus.IsDecomposable.{u_1, u_3} (β : Type u_1) [AddCommMonoid β] (M : outParam (Type u_3)) [AddCommMonoid M]
  [Preorder M] [Modulus β M] : Prop αType u_1 MType u_2]
  [ACouple α.fstEQuasinorm.Couple.fst.{u_1} {α : Type u_1} [AddCommMonoid α] (self : Couple α) : EQuasinorm α.IsSolidEQuasinorm.IsSolid.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [Preorder M] [Modulus β M]
  (B : EQuasinorm β) : Prop] [ACouple α.sndEQuasinorm.Couple.snd.{u_1} {α : Type u_1} [AddCommMonoid α] (self : Couple α) : EQuasinorm α.IsSolidEQuasinorm.IsSolid.{u_1, u_2} {β : Type u_1} {M : Type u_2} [AddCommMonoid β] [Preorder M] [Modulus β M]
  (B : EQuasinorm β) : Prop] (θℝ : ℝReal : Type)
  (qℝ≥0∞ : ℝ≥0∞ENNReal : Type) {δℝ≥0∞ : ℝ≥0∞ENNReal : Type} (hδδ ≠ 0 : δℝ≥0∞ ≠Ne.{u} {α : Sort u} (a b : α) : Prop 0)
  {Nℕ : ℕNat : Type} (hN1 ≤ N : 1 ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop Nℕ) (xα : αType u_1) :
  jInfNormjInfNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (θ : ℝ) (q : ℝ≥0∞) (x : α) : ℝ≥0∞The norm
$$\inf\Bigl\{\,\bigl\|\{2^{-\theta n}J(2^{n},a_{n})\}_{n \in \mathbb{Z}}\bigr\|_{\ell^{q}}
 : a \colon \mathbb{Z} \to \alpha \text{ finitely supported},\ \sum_{n}a_{n}=x\,\Bigr\}.$$  ACouple α θℝ qℝ≥0∞ xα ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop
    discretePhiFunctionalEQuasinorm.discretePhiFunctional (θ : ℝ) (q : ℝ≥0∞) (f : ℤ → ℝ≥0∞) : ℝ≥0∞ θℝ qℝ≥0∞
      (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ(HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ(fun νℤ ↦
            ACouple α.kNormEQuasinorm.Couple.kNorm.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (t : ℝ≥0∞) (x : α) : ℝ≥0∞ (HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ2 ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γνℤ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ 1)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ)HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ xα) +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ
          (IcoSet.Ico.{u_1} {α : Type u_1} [Preorder α] (a b : α) : Set α (Neg.neg.{u} {α : Type u} [self : Neg α] : α → α-Neg.neg.{u} {α : Type u} [self : Neg α] : α → α↑Nℕ)Neg.neg.{u} {α : Type u} [self : Neg α] : α → α ↑Nℕ).indicatorSet.indicator.{u_1, u_3} {α : Type u_1} {M : Type u_3} [Zero M] (s : Set α) (f : α → M) (x : α) : M fun xℤ ↦
            δℝ≥0∞)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ
        boundaryErrorboundaryError.{u_1} {α : Type u_1} [AddCommMonoid α] (A : Couple α) (N : ℕ) (x : α) : ℤ → ℝ≥0∞The error at the two ends of the decomposition of `exists_decomp_Ico_symm`:
$$E_N = 2^{-N}\|x\|_1\,\mathbf{1}_{\{-N\}} + \|x\|_0\,\mathbf{1}_{\{N-1\}}.$$  ACouple α Nℕ xα)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ