formalizing

Stream: new members

[Parivash]

import analysis.specific_limits

lemma some_name (θ : ℕ → ℝ) (a b C P q A V₀ Vads x : ℝ)
  (h1 : ∀ k, θ k = x ^ k * θ 0) (hA : A = ∑' k, θ k)
  (hVads : Vads = V₀ * ∑' k : ℕ, k * θ k) (hq : q = Vads / A) :
  q = a * P / ((1 - b * P) * (1 - b * P + C * P)) :=
begin
  rw hA at hq,
  rw hVads at hq,
  simp_rw h1 at hA,


end

[Patrick Massot]

#backticks

[Parivash]

Hi,
why

rw h1 at hA

doesn't work here?

[Kevin Buzzard]

I don't know what ∑' is -- can you post a #mwe ? But the answer might be "you're trying to rewrite under a binder". Does simp_rw h1 at hA work?

[Kyle Miller]

You can try conv_rhs at hA { congr, funext, rw h1, }, to enter the right-hand side of hA, go inside the sum, then rewrite.

[Kyle Miller]

@Kevin Buzzard "deep recursion was detected at 'whnf' (potential solution: increase stack space in your system)" (probably because of θ 0 on the rhs of the rewrite)

[Parivash]

@Kyle Miller
@Kevin Buzzard
Thanks

[Kevin Buzzard]

yeah that is pretty weird (edit: oh, I see you're right! Of course it gets into an infinite loop :-/ ). Here's a workaround:

lemma some_name (θ : ℕ → ℝ) (a b C P q A V₀ Vads x : ℝ)
  (h1 : ∀ k, θ k = x ^ k * θ 0) (hA : A = ∑' k, θ k)
  (hVads : Vads = V₀ * ∑' k : ℕ, k * θ k) (hq : q = Vads / A) :
  q = a * P / ((1 - b * P) * (1 - b * P + C * P)) :=
begin
  rw hA at hq,
  rw hVads at hq,
  have hA' : A = ∑' k : ℕ, x^k * θ 0,
  { rw hA,
    simp [← h1],
  },

Now hA' is what you were looking for (I hope).

[Kevin Buzzard]

got it:

begin
  rw hA at hq,
  rw hVads at hq,
  simp only [h1] at hA {single_pass := tt},
end

[Parivash]

@Kevin Buzzard
Ohh, Yes, That's the easiest way, Good job
Thanks for taking time