# Zulip Chat Archive

## 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