feat: multiplicative automatic continuity on ℝ

[certik]

This PR adds the multiplicative companion of the existing additive automatic-continuity theorem AddMonoidHom.continuous_of_measurable. See the git commit descriptions for all the details.

Depends on #40976.

AI usage disclosure: I used Claude Opus 4.8 to create the theorems and proofs in my own Lean project, then extracted them into this PR since I think they are general purpose and would be useful for other people. I iterated on the proofs until they are as simple as I could get them. I am new to Lean, so if something should be reworked, please let me know. Lean is amazing, I was able to use it to prove various theorems and check my derivations. This is my little contribution back to the project.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 361bcd9ea7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.MeasureTheory.Measure.Haar.AutomaticContinuity (new file)	2402

---

Declarations diff (regex)

+ AddChar.continuous_of_measurable
+ MeasureTheory.Measure.AddMonoidHom.continuous_of_measurable.
+ continuous_of_measurable_of_mul
+ continuous_of_measurable_of_mul_aux
+ continuous_of_measurable_of_mul_units

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 361bcd9).

• +3 new declarations
• −0 removed declarations

+AddChar.continuous_of_measurable
+continuous_of_measurable_of_mul
+continuous_of_measurable_of_mul_units

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 361bcd9ea7
Reference commit 0ee7df2241

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

[certik]

LLM-generated

[wwylele]

Does it work if you combine AddMonoidHom.continuous_of_measurable with Additive (kˣ) for Monoid k (which includes Field k)? and then you deduce the version that includes zero by special casing it.

In any case, I suspect the current code needs massive cleanup before reviewers are interested in it

[certik]

Does it work if you combine AddMonoidHom.continuous_of_measurable with Additive (kˣ) for Monoid k (which includes Field k)?

I think it doesn't work, I tried:

import Mathlib.MeasureTheory.Measure.Haar.NormedSpace

open MeasureTheory

-- (A) Required codomain instances, general 𝕜:
example {𝕜 : Type*} [RCLike 𝕜] : SeminormedAddCommGroup (Additive 𝕜ˣ) := inferInstance
example {𝕜 : Type*} [RCLike 𝕜] : NormedSpace ℝ (Additive 𝕜ˣ) := inferInstance

-- (B) Concretely at 𝕜 = ℂ and 𝕜 = ℝ:
example : SeminormedAddCommGroup (Additive ℂˣ) := inferInstance
example : NormedSpace ℝ (Additive ℂˣ) := inferInstance
example : NormedSpace ℝ (Additive ℝˣ) := inferInstance

-- (C) The full reduction: bundle a measurable multiplicative `f : ℝ → 𝕜ˣ` as
--     `ℝ →+ Additive 𝕜ˣ` and feed it to the additive theorem. (Side proof
--     obligations are `sorry`; we only care whether the theorem can apply.)
example {𝕜 : Type*} [RCLike 𝕜] [MeasurableSpace 𝕜] [BorelSpace 𝕜]
    {f : ℝ → 𝕜ˣ} (hmeas : Measurable f)
    (hmul : ∀ x y, f (x + y) = f x * f y) : Continuous f := by
  let F : ℝ →+ Additive 𝕜ˣ :=
    { toFun := fun x => Additive.ofMul (f x)
      map_zero' := by sorry
      map_add' := by sorry }
  have hcont : Continuous F :=
    MeasureTheory.Measure.AddMonoidHom.continuous_of_measurable F (by sorry)
  sorry

and get:

$ lake env lean combine_experiment.lean
combine_experiment.lean:6:73: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  SeminormedAddCommGroup (Additive 𝕜ˣ)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
combine_experiment.lean:7:33: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  SeminormedAddCommGroup (Additive 𝕜ˣ)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
combine_experiment.lean:10:50: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  SeminormedAddCommGroup (Additive ℂˣ)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
combine_experiment.lean:11:10: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  SeminormedAddCommGroup (Additive ℂˣ)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
combine_experiment.lean:12:10: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  SeminormedAddCommGroup (Additive ℝˣ)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
combine_experiment.lean:25:4: error: Type mismatch
  Measure.AddMonoidHom.continuous_of_measurable ?m.53 sorry
has type
  Continuous ⇑?m.53
but is expected to have type
  Continuous ⇑F

The reason is that AddMonoidHom.continuous_of_measurable requires a NormedSpace ℝ codomain, but Additive 𝕜ˣ  cannot carry that structure because it isn't an ℝ-vector space.

[wwylele]

I recommend splitting the change in Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean to a new PR as it is possibly less controversial and can probably go through faster review

[certik]

I recommend splitting the change in Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean to a new PR as it is possibly less controversial and can probably go through faster review

Good idea, I posted it here: #40976

I also based on your previous comment I cleaned up this PR a little bit in b33bec6, I didn't need the f 0 ≠ 0 condition.

If you point me roughly what kind of areas to focus on to clean it up --- the theorems themselves, or their proofs, or the theorem assumptions, etc., I'll do it.

[wwylele]

Here is an example how to make the proof more natural and less like AI-generated. I personally call them have-folding and have-inverting. The goal is to have as little indentation as possible, by inlining haves, or rearange proof order so that the big chunk of have proof becomes the main proof body. Here, I noticed that we are converting the goal to Continuous fun s ↦ (F (s + a) - F s) / F a , which itself has a very short proof (I also shortened it to fun_prop), so that comes first. I then use convert to say "it now suffices to show f and Continuous fun s ↦ (F (s + a) - F s) / F a are equal, so what was previously in a large have block is now the only main goal

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.