Redefine real powers of `NNReal` numbers

As discussed with @hrmacbeth today, it's strange that the definition of L1 space depends on the complex logarithm (and trigonometry). Heather suggested that we redefine x ^ y for x : ℝ≥0 and y : ℝ with fewer dependencies. We discussed two approaches:

Use exp and log

We define

instance Pow ℝ≥0 ℝ where
  pow x y := ⟨exp (y * Real.log x), exp_nonneg _⟩

or with some if/else if there are special cases like 0 ^ 0 where this doesn't give the answer we want.

Then we prove properties of this function directly without relying on x ^ y for real x and y. This approach needs less work but still leaves heavy dependencies.

Use rational powers

We define

instance Pow ℝ≥0 ℚ where
  pow x r := (NNReal.powOrderIso r.den r.den_nz).symm (x ^ r.num)

instance Pow ℝ≥0 ℝ where
  pow x y :=
    if h : ∃ z, Tendsto (x ^ ·) (comap Rat.cast (𝓝 y)) (𝓝 z)
	then z else 0

This approach needs more work but makes the definition of L¹
independent of exp.

Start by comparing the two proposed definitions for real powers on NNReal: the exp/log approach and the rational-power limit approach. Determine which approach should be adopted, including the required special cases and properties. Done means NNReal powers are redefined and the definition of L¹ no longer depends on the complex logarithm or trigonometry.