using change of variables

Stream: new members

[Nicholas Wilson]

I understand the statement of the theorem for a change, but how do I actually use [integral_comp_smul_deriv}(https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Integral/FundThmCalculus.html#intervalIntegral.integral_comp_smul_deriv)? In this case to perform the change of variables (x,y)→ ((u+v)/2,((u-v)/2).

import Mathlib
open Real
example (a : ℝ )(s : Set ℝ) : ∫(x :ℝ )(y:ℝ) in s, cos (a*x)* cos (a*y) + (sin a*y)* sin (a*x) = 0 := by sorry

(=0 because the RHS is irrelevant).

[Kevin Buzzard]

The lemma you link to seems to only let you change one real variable, so if you want to change two then you probably need another lemma? I'm pretty sure this lemma exists because I saw Sebastian Gouezel change 2 variables in a nice talk in Lean in Lyon (available on YouTube)

[Nicholas Wilson]

I'm pretty sure you can decompose this change into two one-variable changes,

(x,y) = (A/2)*(u,v)

then you can do an LU decomposition of

A/2=[[1,1],  [1, -1]]
L=[[1,0], [1,1]]
U=[[1,1], [0,2]]

and L,U are one- variable-at-a-time changes.

[Patrick Massot]

We don't need this trick, we have a super general change of variables formula.

[Nicholas Wilson]

Link?

[Patrick Massot]

https://leanprover-community.github.io/mathlib-overview.html or https://leanprover-community.github.io/undergrad.html are the very first place to look at, and they both answer your question. Mathematics in Lean also works. Searching for "change of variable" in the Mathlib folder also works. Sometimes finding stuff in Mathlib is hard, but you need to try something.

[Nicholas Wilson]

I found the one linked upstream from the undergrad page, I had presumed you meant one of the other theorems listed alongside it and was wondering which ones you were referring to.

[Nicholas Wilson]

I have found the video referred to and am watching it but the combination of accent, video and audio quality make that slow going.

[Patrick Massot]

You don't need to video to find that result in Mathlib.

[Nicholas Wilson]

No, but it might tell me how to use it:
which direction I want to perform the substitution in,
how I should write the bounds or form the function composition (depending on which order I want it to go in),
how I should provide the assumption necessary
how to rw [\l one_mul] to form the multiplication by the derivative, since naive application fails with

tactic 'rewrite' failed, pattern is a metavariable
  ?a
from equation
  ?a = 1 * ?a

[Damiano Testa]

For this last error, try telling Lean what is the variable that you want to multiply by one.

[Nicholas Wilson]

Silly question, how? I currently have

conv =>
  enter[1,2]
  ext
  enter [2]
  ext
  rw [\l mul_one] -- error

state is | cos (a * x✝¹) * cos (a * x✝) + sin a * x✝ * sin (a * x✝¹).
rw [mul_one at cos (a * x¹) * cos (a * x) + sin a * x * sin (a * ✝¹)] didn't work neither did rw [\l mul_one] at h.h.

[Damiano Testa]

Neither Lean nor I have any idea of which variable you are trying to multiply by 1. The syntax to pass an explicit variable to a lemma is to put that variable as an argument to the lemma: rw [\l mul_one <insert your variable here>].

[Nicholas Wilson]

The whole state expression, I want to get (cos (a * x✝¹) * cos (a * x✝) + sin a * x✝ * sin (a * x✝¹))*1

[Damiano Testa]

rw [← mul_one (_ + _)] this works: it is a hint to Lean that it should try to unify the metavariable that it does not know with something that has an addition in it.