feat: fun_prop lemmas for GL n R and SL n R

[j-loreaux]

These lemmas allow fun_prop to prove that evaluating a continuous function into the general or special linear groups at an entry is continuous.

This also adds fun_prop to UpperHalfPlane.{num,denom}, Continuous.matrixVecCons and and new lemma Continuous.matrixOf and uses all these to golf some proofs of continuity regarding the action of SL 2 ℝ on ℍ from a recent PR.

For good measure, we add fun_prop to a number of other lemmas which should be tagged.

---

[github-actions]

PR summary fb17c7c573

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Continuous.matrixOf
+ continuous_matrixOf
+ denom_continuous
+ num_continuous
++ continuous_apply

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[loefflerd]

This is a great improvement, thanks! It's a pity it conflicts with #37601 but there's no way that could have been avoided (I opened that a matter of minutes ago).

[loefflerd]

Probably the all_goals can be replaced by a second <;> on prev line (github won't let me suggest across a deleted code block). Can the long simp only be replaced using the suffices foo by simp idiom?

[j-loreaux]

Here are two alternatives for the proof. The first way is super short, but it's effectively a way to cheat and not get a linter warning from simp. If we're not allowed to do simp; fun_prop, then I can't really see a way this would be allowed.

  refine continuous_induced_rng.mpr (continuous_matrix fun i j ↦ ?_)
  fin_cases i <;> fin_cases j <;> simpa using by fun_prop (disch := grind [im_pos])

The other way uses your suffices suggestion, but the annoying bit is that you have spell out all 4 of the continuity goals. Nevertheless, this is probably the "correct" solution.

  suffices Continuous (fun a : ℍ ↦ √a.im) ∧ (Continuous fun a : ℍ ↦ a.re / √a.im)
      ∧ (Continuous fun a : ℍ ↦ (0 : ℝ)) ∧ Continuous (fun a : ℍ ↦ (√a.im)⁻¹) by
    refine continuous_induced_rng.mpr (continuous_matrix fun i j ↦ ?_)
    fin_cases i <;> fin_cases j <;> simp_all
  refine ⟨?_, ?_, ?_, ?_⟩ <;> fun_prop (disch := grind [im_pos])

Let me know which one you prefer.

[j-loreaux]

There is potentially one other thing that's possible, although I don't really want to implement it. Note that:

  apply continuous_induced_rng.mpr
  simp only [Function.comp_def, coe_toSL2R, one_div]
  -- ⊢ Continuous fun x ↦ !![√x.im, x.re / √x.im; 0, (√x.im)⁻¹]

and we could potentially have a simproc (which I'll call continuousMatrix) for turning this goal into the 4 conjuncted goals. Then the proof would simplify to:

  apply continuous_induced_rng.mpr
  simp only [Function.comp_def, coe_toSL2R, one_div, continuousMatrix]
  refine ⟨?_, ?_, ?_, ?_⟩ <;> fun_prop (disch := grind [im_pos])

[loefflerd]

Thanks for putting in the effort to look for a clean solution, but I'm actually not sure any of these are better than your first approach (with the long simp only). I suspect the simpa using by fun_prop (disch := grind [...]) would be a bit "brittle", and writing a simproc sounds like a lot of work. I propose we just stick with the first approach.

[j-loreaux]

Actually, a simproc is more than we need. Just a few small lemmas can get us there:

import Mathlib

open Matrix 

variable {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]

@[simp]
lemma continuous_to_fin_zero {f : β → Fin 0 → α} : Continuous f := by
  rw [Subsingleton.elim f (fun _ ↦ Classical.arbitrary (Fin 0 → α))]
  exact continuous_const

@[simp]
lemma Continuous.to_vecCons {n : Nat} {g : β → α} {f : β → Fin n → α} :
    Continuous (fun x : β ↦ vecCons (g x) (f x)) ↔
      Continuous f ∧ Continuous g := by
  sorry

lemma Continuous.matrixOf {m n : Nat} {f : β → Fin m → Fin n → α} :
    Continuous (fun x : β ↦ Matrix.of (f x)) ↔ Continuous f := by
  rfl

example : Continuous (fun x : ℝ ↦ ![√x, x ^ 2]) ↔
    Continuous (· ^ 2 : ℝ → ℝ) ∧ Continuous Real.sqrt := by
  simp

example : Continuous (fun x : ℝ ↦ !![√x, x ^ 2; x + 1, x - 1]) ↔
    ((Continuous fun x : ℝ => x - 1) ∧ Continuous fun x : ℝ => x + 1) ∧
    (Continuous fun x : ℝ => x ^ 2) ∧ Continuous Real.sqrt := by
  simp [Continuous.matrixOf]

I'll finish these later and improve the proof afterwards.

[j-loreaux]

Oh! even better, we can just tag Continuous.matrixVecCons with fun_prop and I think doing so makes total sense.