## Stream: general

### Topic: Stating a theorem involving two bit0 / bit1

#### Heather Macbeth (Dec 26 2021 at 00:40):

Is there a way to state a single theorem which generalizes all the following theorems?

import measure_theory.function.lp_space

open measure_theory
open_locale ennreal

variables {E : Type*} [measurable_space E] [normed_group E]
variables {α : Type*} [measurable_space α] (f : α → E) (μ : measure_theory.measure α)

example (hf : mem_ℒp f 2 μ) : ∫⁻ x, ∥f x∥₊ ^ 2 ∂μ < ∞ :=
begin
convert lintegral_rpow_nnnorm_lt_top_of_snorm_lt_top _ _ hf.snorm_lt_top,
{ norm_cast },
{ norm_num },
{ norm_num }
end

example (hf : mem_ℒp f 3 μ) : ∫⁻ x, ∥f x∥₊ ^ 3 ∂μ < ∞ :=
begin
convert lintegral_rpow_nnnorm_lt_top_of_snorm_lt_top _ _ hf.snorm_lt_top,
{ norm_cast },
{ norm_num },
{ norm_num }
end

example (hf : mem_ℒp f 4 μ) : ∫⁻ x, ∥f x∥₊ ^ 4 ∂μ < ∞ :=
begin
convert lintegral_rpow_nnnorm_lt_top_of_snorm_lt_top _ _ hf.snorm_lt_top,
{ norm_cast },
{ norm_num },
{ norm_num }
end

...


#### Heather Macbeth (Dec 26 2021 at 00:41):

The point is that, taking the first one as an example,

example (hf : mem_ℒp f 2 μ) : ∫⁻ x, ∥f x∥₊ ^ 2 ∂μ < ∞ :=


the first 2 is an ennreal 2, and the second 2 is a nat 2.

#### Heather Macbeth (Dec 26 2021 at 00:42):

So the theorem statement I want is, "given a particular sequence s of bit0 and bit1 applications, if f is in Lp of the ennreal constructed from s, then a certain thing involving the nat constructed from s is bounded."

#### Eric Rodriguez (Dec 26 2021 at 00:46):

why doesn't (n : nat) (hf : blah (n : ennreal)) work?

#### Yury G. Kudryashov (Dec 26 2021 at 00:54):

Because coercion from nat to ennreal is not defeq to the corresponding number literal.

#### Eric Rodriguez (Dec 26 2021 at 00:55):

okay, sure, but it's 1 rw

#### Eric Rodriguez (Dec 26 2021 at 00:55):

or is that really annoying? idk how this part of the library works

#### Yury G. Kudryashov (Dec 26 2021 at 01:02):

@Heather Macbeth Do you really need defeq here?

#### Yury G. Kudryashov (Dec 26 2021 at 01:03):

You can easily prove a version with nat, pow, and coe.

#### Yury G. Kudryashov (Dec 26 2021 at 01:04):

It will only assume n ≠ 0.

#### Heather Macbeth (Dec 26 2021 at 01:05):

This is a toy example (actually it will be for the new Lp spaces in #11015). I only need the 2 version (it's to simplify repeatedly-occuring calculations for inner product spaces, and I'd like to have it available for dot notation). But it's a bit sad to state just the 2 version if there somehow is a way to express the general version.

#### Yury G. Kudryashov (Dec 26 2021 at 01:07):

You can formulate it for nat and coe, then specialize (with simpa using ... or exact_mod_cast).

#### Yury G. Kudryashov (Dec 26 2021 at 01:08):

AFAIK, in Lean 4 number literals are implemented using coercion from Nat.

#### Heather Macbeth (Dec 26 2021 at 01:08):

I was hoping there was something clever involving docs#parser.numeral or suchlike.

#### Heather Macbeth (Dec 26 2021 at 01:12):

Yury G. Kudryashov said:

AFAIK, in Lean 4 number literals are implemented using coercion from Nat.

But this is interesting, I guess it means there'd be a limited shelf-life for such a trick even if it did exist.

Last updated: Aug 03 2023 at 10:10 UTC