Trouble with Exponents in Integral Proof

Stream: new members

[Colin Jones ⚛️]

I am having two difficulties with this proof shown below.

import Mathlib

open Real MeasureTheory

theorem long_range_correction_equality (hr : 0 < rc) (ρ ε σ : ℝ) :
    (2 * π * ρ) * ∫ (r : ℝ) in Set.Ioi rc, 4 * ε * (r ^ (2:ℝ) * (((σ / r) ^ (12:ℝ)) -
    ((σ / r) ^ (6:ℝ)))) = (8 * π * ρ * ε) * ((1/9) * (σ ^ (12:ℝ) / rc ^ (9:ℝ) -
    (1/3) * σ ^ (6:ℝ) / rc ^ (3:ℝ))) := by
  by_cases hρ : ρ = 0
  · simp only [hρ, mul_zero, zero_mul]
  · by_cases hε : ε = 0
    · simp only [hε, mul_zero, zero_mul, integral_zero, mul_zero]
    · calc
        2 * π * ρ * ∫ (r : ℝ) in Set.Ioi rc, 4 * ε * (r ^ (2:ℝ) * ((σ / r) ^ (12:ℝ) -
          (σ / r) ^ (6:ℝ))) =
        (2 * π * ρ) * (∫ (r : ℝ) in Set.Ioi rc, ((r ^ (2:ℝ) *
          ((σ / r) ^ (12:ℝ) - (σ / r) ^ (6:ℝ))) • (4 * ε))) := by
            field_simp
            congr with x
            ring
        _ = (8 * π * ρ * ε)  * ∫ (r : ℝ) in Set.Ioi rc, (r ^ (2:ℝ) *
          ((σ / r) ^ (12:ℝ) - (σ / r) ^ (6:ℝ))) := by
            rw [integral_smul_const, smul_eq_mul]
            ring
      rw [mul_eq_mul_left_iff]
      left
      calc
        ∫ (r : ℝ) in Set.Ioi rc, r ^ (2:ℝ) * ((σ / r) ^ (12:ℝ) - (σ / r) ^ (6:ℝ)) =
          ∫ (r : ℝ) in Set.Ioi rc, (σ ^ (12:ℝ) * r ^ (-10:ℝ) - σ ^ (6:ℝ) * r ^ (-4:ℝ)) := by
            congr with x
            rw [div_eq_mul_inv]
            rw [show (-10:ℝ) = 2 + - 12 by norm_num, show (-4:ℝ) = 2 + - 6 by norm_num]

First, is there a way to tell lean every number I use is a real number instead of me having to type-set everything?

Second, I'm having trouble proving the last goal I have in the calc block because Lean can't verify that sigma and x^-1 are not greater than zero. It's possible that sigma isn't, but that shouldn't matter as the power I'm raising the terms of (σ * x⁻¹) are technically natural numbers. The proof that (σ * x⁻¹) ^ 6 = (σ ^ 6 * x⁻¹ ^ 6) (represented by mul_pow) shouldn't require that sigma and x^-1 be greater than zero as 6 is a natural number, but I haven't found a way to tell Lean that.

[Colin Jones ⚛️]

I'd prefer everything to be in real numbers except for specific circumstances like the subgoal I want to prove. Is there a consistent way to convert numbers in Lean without going through lines and lines of proof?

[Aaron Liu]

Colin Jones ⚛️ said:

It's possible that sigma isn't, but that shouldn't matter as the power I'm raising the terms of (σ * x⁻¹) are technically natural numbers. The proof that (σ * x⁻¹) ^ 6 = (σ ^ 6 * x⁻¹ ^ 6) (represented by mul_pow) shouldn't require that sigma and x^-1 be greater than zero as 6 is a natural number, but I haven't found a way to tell Lean that.

You should use docs#Real.rpow_natCast to rewrite the powers to a natural number, then use docs#mul_pow to distribute.

[Aaron Liu]

Colin Jones ⚛️ said:

First, is there a way to tell lean every number I use is a real number instead of me having to type-set everything?

Yes. I wouldn't recommend it, as you can't turn it off after and I think it has the potential to break a lot of things.
See #lean4 > Numeric literals

[Colin Jones ⚛️]

rw [show (σ * x⁻¹) ^ (12:ℝ) = (σ * x⁻¹) ^ (12:ℕ) by rw [rpow_natCast (σ * x⁻¹) (12)]]
This is having some trouble

[Colin Jones ⚛️]

I think it's because the (12:ℝ) isn't recognized as ↑12 in Lean

[Aaron Liu]

You also need docs#Nat.cast_ofNat

[Colin Jones ⚛️]

Thank you! I got it to work.

[Colin Jones ⚛️]

Aaron Liu said:

Colin Jones ⚛️ said:

First, is there a way to tell lean every number I use is a real number instead of me having to type-set everything?

Yes. I wouldn't recommend it, as you can't turn it off after and I think it has the potential to break a lot of things.
See #lean4 > Numeric literals

I tried the macro they had there but it didn't seem to work for exponents, but I will take your advice and manually define my numbers as real.

[Colin Jones ⚛️]

theorem long_range_correction_equality (hr : 0 < rc) (hσ : 0 ≤ σ) (ρ ε σ : ℝ) :
    (2 * π * ρ) * ∫ (r : ℝ) in Set.Ioi rc, 4 * ε * (r ^ (2:ℝ) * (((σ / r) ^ (12:ℝ)) -
    ((σ / r) ^ (6:ℝ)))) = (8 * π * ρ * ε) * ((1/9) * (σ ^ (12:ℝ) / rc ^ (9:ℝ) -
    (1/3) * σ ^ (6:ℝ) / rc ^ (3:ℝ))) := by
  by_cases hρ : ρ = 0
  · simp only [hρ, mul_zero, zero_mul]
  · by_cases hε : ε = 0
    · simp only [hε, mul_zero, zero_mul, integral_zero, mul_zero]
    · calc
        2 * π * ρ * ∫ (r : ℝ) in Set.Ioi rc, 4 * ε * (r ^ (2:ℝ) * ((σ / r) ^ (12:ℝ) -
          (σ / r) ^ (6:ℝ))) =
        (2 * π * ρ) * (∫ (r : ℝ) in Set.Ioi rc, ((r ^ (2:ℝ) *
          ((σ / r) ^ (12:ℝ) - (σ / r) ^ (6:ℝ))) • (4 * ε))) := by
            field_simp
            congr with x
            ring
        _ = (8 * π * ρ * ε)  * ∫ (r : ℝ) in Set.Ioi rc, (r ^ (2:ℝ) *
          ((σ / r) ^ (12:ℝ) - (σ / r) ^ (6:ℝ))) := by
            rw [integral_smul_const, smul_eq_mul]
            ring
      rw [mul_eq_mul_left_iff]
      left
      calc
        ∫ (r : ℝ) in Set.Ioi rc, r ^ (2:ℝ) * ((σ / r) ^ (12:ℝ) - (σ / r) ^ (6:ℝ)) =
          ∫ (r : ℝ) in Set.Ioi rc, (σ ^ (12:ℝ) * r ^ (-10:ℝ) + - σ ^ (6:ℝ) * r ^ (-4:ℝ)) := by
            congr with x
            rw [div_eq_mul_inv, show (-10:ℝ) = 2 + - 12 by norm_num, show (-4:ℝ) = 2 + - 6 by
              norm_num, show (σ * x⁻¹) ^ (12:ℝ) = (σ * x⁻¹) ^ (12:ℕ) by rw [← Nat.cast_ofNat,
              rpow_natCast (σ * x⁻¹) (12)], show (σ * x⁻¹) ^ (6:ℝ) = (σ * x⁻¹) ^ (6:ℕ) by
              rw [← Nat.cast_ofNat, rpow_natCast (σ * x⁻¹) (6)], mul_pow, mul_pow]
            have h1 : x⁻¹ ^ 12 = x ^ (-12:ℝ) := by
              norm_cast
              simp only [inv_pow, zpow_negSucc]
            have h2 : x⁻¹ ^ 6 = x ^ (-6:ℝ) := by
              norm_cast
              simp only [inv_pow, zpow_negSucc]
            rw [h1, h2, rpow_add, rpow_add, show σ ^ 6 = σ ^ (6:ℝ) by norm_cast, show σ ^ 12 =
              σ ^ (12:ℝ) by norm_cast]
            ring

In the proof, how do I show from congr that x > r_c > 0?