Stating a theorem involving two `bit0` / `bit1`

Stream: general

[Heather Macbeth]

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]

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]

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]

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

[Yury G. Kudryashov]

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

[Eric Rodriguez]

okay, sure, but it's 1 rw

[Eric Rodriguez]

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

[Yury G. Kudryashov]

@Heather Macbeth Do you really need defeq here?

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

It will only assume n ≠ 0.

[Heather Macbeth]

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]

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

[Yury G. Kudryashov]

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

[Heather Macbeth]

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

[Heather Macbeth]

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.