6. The Aoki-Rolewicz theorem🔗

Definition2.23

Statement uses 2

Statement dependency previews

Preview

Definition 2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 1

Reverse dependency previews

Preview

Theorem 1.2.1

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

⚠L∃∀N

Lean code for Definition2.23●1 definition, incomplete

defdefined in MultilinearInterpolation/AokiRolewicz.lean

contains sorry

def EQuasinorm.aokiRolewicz.{u_1}EQuasinorm.aokiRolewicz.{u_1} {α : Type u_1} [AddCommMonoid α] (A : EQuasinorm α) (p : ℝ) (hp : (2 * A.C) ^ p = 2) :
  ESeminorm α {α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]
  (AEQuasinorm α : EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 αType u_1) (pℝ : ℝReal : Type) (hp(2 * A.C) ^ p = 2 : (HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ2 *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ AEQuasinorm α.CEQuasinorm.C.{u_1} {α : Type u_1} [AddCommMonoid α] (self : EQuasinorm α) : ℝ≥0∞)HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ pℝ =Eq.{u_1} {α : Sort u_1} : α → α → Prop 2) : ESeminormESeminorm.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 αType u_1

def EQuasinorm.aokiRolewicz.{u_1}EQuasinorm.aokiRolewicz.{u_1} {α : Type u_1} [AddCommMonoid α] (A : EQuasinorm α) (p : ℝ) (hp : (2 * A.C) ^ p = 2) :
  ESeminorm α
  {α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]
  (AEQuasinorm α : EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 αType u_1) (pℝ : ℝReal : Type)
  (hp(2 * A.C) ^ p = 2 : (HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ2 *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ AEQuasinorm α.CEQuasinorm.C.{u_1} {α : Type u_1} [AddCommMonoid α] (self : EQuasinorm α) : ℝ≥0∞)HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ pℝ =Eq.{u_1} {α : Sort u_1} : α → α → Prop 2) : ESeminormESeminorm.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 αType u_1

Theorem1.2.1

Statement uses 4

Statement dependency previews

Preview

Definition 2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0⚠L∃∀N

Lean code for Theorem1.2.1●1 theorem, incomplete

theoremdefined in MultilinearInterpolation/AokiRolewicz.lean

contains sorry

theorem aokiRolewicz_equiv_pow.{u_1}aokiRolewicz_equiv_pow.{u_1} {α : Type u_1} [AddCommMonoid α] {A : EQuasinorm α} {p : ℝ} (hp : (2 * A.C) ^ p = 2) :
  (A.aokiRolewicz p hp).toEQuasinorm ≈ A.pow ⋯ {α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]
  {AEQuasinorm α : EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 αType u_1} {pℝ : ℝReal : Type} (hp(2 * A.C) ^ p = 2 : (HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ2 *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ AEQuasinorm α.CEQuasinorm.C.{u_1} {α : Type u_1} [AddCommMonoid α] (self : EQuasinorm α) : ℝ≥0∞)HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ pℝ =Eq.{u_1} {α : Sort u_1} : α → α → Prop 2) :
  (AEQuasinorm α.aokiRolewiczEQuasinorm.aokiRolewicz.{u_1} {α : Type u_1} [AddCommMonoid α] (A : EQuasinorm α) (p : ℝ) (hp : (2 * A.C) ^ p = 2) :
  ESeminorm α pℝ hp(2 * A.C) ^ p = 2).toEQuasinormESeminorm.toEQuasinorm.{u_1} {α : Type u_1} [AddCommMonoid α] (self : ESeminorm α) : EQuasinorm α ≈HasEquiv.Equiv.{u, v} {α : Sort u} [self : HasEquiv α] : α → α → Sort v AEQuasinorm α.powEQuasinorm.pow.{u_1} {α : Type u_1} [AddCommMonoid α] (A : EQuasinorm α) {p : ℝ} (hp : 0 < p) : EQuasinorm α ⋯

theorem aokiRolewicz_equiv_pow.{u_1}aokiRolewicz_equiv_pow.{u_1} {α : Type u_1} [AddCommMonoid α] {A : EQuasinorm α} {p : ℝ} (hp : (2 * A.C) ^ p = 2) :
  (A.aokiRolewicz p hp).toEQuasinorm ≈ A.pow ⋯
  {α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]
  {AEQuasinorm α : EQuasinormEQuasinorm.{u_1} (α : Type u_1) [AddCommMonoid α] : Type u_1 αType u_1} {pℝ : ℝReal : Type}
  (hp(2 * A.C) ^ p = 2 : (HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ2 *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ AEQuasinorm α.CEQuasinorm.C.{u_1} {α : Type u_1} [AddCommMonoid α] (self : EQuasinorm α) : ℝ≥0∞)HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ pℝ =Eq.{u_1} {α : Sort u_1} : α → α → Prop 2) :
  (AEQuasinorm α.aokiRolewiczEQuasinorm.aokiRolewicz.{u_1} {α : Type u_1} [AddCommMonoid α] (A : EQuasinorm α) (p : ℝ) (hp : (2 * A.C) ^ p = 2) :
  ESeminorm α pℝ hp(2 * A.C) ^ p = 2).toEQuasinormESeminorm.toEQuasinorm.{u_1} {α : Type u_1} [AddCommMonoid α] (self : ESeminorm α) : EQuasinorm α ≈HasEquiv.Equiv.{u, v} {α : Sort u} [self : HasEquiv α] : α → α → Sort v
    AEQuasinorm α.powEQuasinorm.pow.{u_1} {α : Type u_1} [AddCommMonoid α] (A : EQuasinorm α) {p : ℝ} (hp : 0 < p) : EQuasinorm α ⋯