function with finite norm

Stream: new members

[Nicholas Wilson]

how do I formulate the hypothesis that a function f has finite norm?
I have tried ( hi : ∫ x , f x > 0 ∧ ∫ x , f x < ∞) which results in expected token and Real.infinity which results in unknown constant

[Eric Wieser]

The ∞ symbol requires open scoped ENNReal, but without an #mwe it's hard to tell whether that will help you

[Nicholas Wilson]

pardon my ignorance, what is #mwe what does it do?

[Nicholas Wilson]

open ENNReal seems to have worked.

[Eric Wieser]

Nicholas Wilson said:

pardon my ignorance, what is #mwe what does it do?

It is a link that you can click

[Eric Wieser]

Nicholas Wilson said:

open ENNReal seems to have worked.

It's very likely you have written a vacuous assumption like "the following is finite: the norm, if the norm is finite, else 0 if it is not"

[Nicholas Wilson]

It would appear so, it renders ins the info view as hi: ∫ (x : ℝ), f x > 0 ∧ sorryAx Prop true

[Eric Wieser]

If sorryAx appears that usual means you have ignored a previous error message

[Nicholas Wilson]

Ah, that was a trailing error for unterminated := by I now get

type mismatch
  ⊤
has type
  ℝ≥0∞ : Type
but is expected to have type
  ℝ : Type

for the expression (∫ x , f x ) < ∞ )
The example usage

theorem anti_symmetry { f : ℝ → ℝ  } { x y  : ℝ }
    ( hpos : (f x) ≥ 0 ) --positive
    ( hi : ( ∫ x , (f x) > 0) ∧ (∫ x , f x ) < ∞ ) --finite integral
    ( hy : y ≥ 0)   ( hzge : (f y)  = 0) -- zero on the positive real line
:
    ∫ x, ((f x) - f (-x )) = 0 -- total integral is zero
:= by sorry

[Nicholas Wilson]

with open ENNReal

[Patrick Massot]

You really need to read #mwe and follow instructions there.

[Nicholas Wilson]

I don't have a working example because I get an error and there is not much left to remove from that.

Things I have tried that don't work:
changed the Type of f to { f : ℝ → NNReal } doesn't work because failed to synthesize instance NormedAddCommGroup NNReal and can't do integrals on them. Same for ENNReal, EReal.
Trying to coerce the type of ∫ x, f x to ENNReal with ↑(∫ x, f x ) (not sure if I did that correctly though).
Interestingly opening EReal while having ENNReal be not opened gives invalid token error for ∞.

[Patrick Massot]

I'm afraid that reading the title of that #mwe webpage is not enough, you also need to read at least the first sentence.

[Patrick Massot]

I case you already posted a code snippet such as the one you posted here you can check whether you followed instruction by simply clicking the "View in Lean 4 playground" link that appear in the upper-right corner of the code block. In your case this bring you there where you will see that your snippet isn't a #mwe since it doesn't reproduce the problem you are facing on your computer.