From 3cf5aad73340e093c8e75d8317a39c1803133d53 Mon Sep 17 00:00:00 2001 From: Xavier Roblot Date: Mon, 2 Dec 2024 18:58:37 +0000 Subject: [PATCH] feat(Analysis/BoxIntegral/UnitPartition): Prove results linking integral point counting and integrals (#12405) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We prove the following result: > Let `s` be a bounded, measurable set of `ι → ℝ` whose frontier has zero volume and let `F` be a > continuous function. Then the limit as `n → ∞` of `∑ F x / n ^ card ι`, where the sum is over the > points in `s ∩ n⁻¹ • (ι → ℤ)`, tends to the integral of `F` over `s`. using Riemann integration. As a special case, we deduce that > The limit as `n → ∞` of `card (s ∩ n⁻¹ • (ι → ℤ)) / n ^ card ι` tends to the volume of `s`. Both of these statements are for a variable `n : ℕ`. However, with the additional hypothesis: `x • s ⊆ y • s` whenever `0 < x ≤ y`, we generalize the previous statement to a real variable. This PR is part of the proof of the Analytic Class Number Formula. Co-authored-by: Xavier Roblot <46200072+xroblot@users.noreply.github.com> --- Mathlib/Algebra/Group/Indicator.lean | 10 +- Mathlib/Algebra/Module/ZLattice/Basic.lean | 15 +- .../Analysis/BoxIntegral/UnitPartition.lean | 197 +++++++++++++++++- Mathlib/LinearAlgebra/Basis/Basic.lean | 4 + Mathlib/Topology/ContinuousOn.lean | 12 ++ 5 files changed, 233 insertions(+), 5 deletions(-) diff --git a/Mathlib/Algebra/Group/Indicator.lean b/Mathlib/Algebra/Group/Indicator.lean index 8dfed5c563fb9f..604906c6e8770b 100644 --- a/Mathlib/Algebra/Group/Indicator.lean +++ b/Mathlib/Algebra/Group/Indicator.lean @@ -120,9 +120,17 @@ set. -/ theorem mem_of_mulIndicator_ne_one (h : mulIndicator s f a ≠ 1) : a ∈ s := not_imp_comm.1 (fun hn => mulIndicator_of_not_mem hn f) h -@[to_additive] +/-- See `Set.eqOn_mulIndicator'` for the version with `sᶜ`. -/ +@[to_additive + "See `Set.eqOn_indicator'` for the version with `sᶜ`"] theorem eqOn_mulIndicator : EqOn (mulIndicator s f) f s := fun _ hx => mulIndicator_of_mem hx f +/-- See `Set.eqOn_mulIndicator` for the version with `s`. -/ +@[to_additive + "See `Set.eqOn_indicator` for the version with `s`."] +theorem eqOn_mulIndicator' : EqOn (mulIndicator s f) 1 sᶜ := + fun _ hx => mulIndicator_of_not_mem hx f + @[to_additive] theorem mulSupport_mulIndicator_subset : mulSupport (s.mulIndicator f) ⊆ s := fun _ hx => hx.imp_symm fun h => mulIndicator_of_not_mem h f diff --git a/Mathlib/Algebra/Module/ZLattice/Basic.lean b/Mathlib/Algebra/Module/ZLattice/Basic.lean index cadfde60a11798..741fa6f4df8065 100644 --- a/Mathlib/Algebra/Module/ZLattice/Basic.lean +++ b/Mathlib/Algebra/Module/ZLattice/Basic.lean @@ -62,11 +62,17 @@ variable (b : Basis ι K E) theorem span_top : span K (span ℤ (Set.range b) : Set E) = ⊤ := by simp [span_span_of_tower] - theorem map {F : Type*} [NormedAddCommGroup F] [NormedSpace K F] (f : E ≃ₗ[K] F) : Submodule.map (f.restrictScalars ℤ) (span ℤ (Set.range b)) = span ℤ (Set.range (b.map f)) := by simp_rw [Submodule.map_span, LinearEquiv.restrictScalars_apply, Basis.coe_map, Set.range_comp] +open scoped Pointwise in +theorem smul {c : K} (hc : c ≠ 0) : + c • span ℤ (Set.range b) = span ℤ (Set.range (b.isUnitSMul (fun _ ↦ hc.isUnit))) := by + rw [smul_span, Set.smul_set_range] + congr! + rw [Basis.isUnitSMul_apply] + /-- The fundamental domain of the ℤ-lattice spanned by `b`. See `ZSpan.isAddFundamentalDomain` for the proof that it is a fundamental domain. -/ def fundamentalDomain : Set E := {m | ∀ i, b.repr m i ∈ Set.Ico (0 : K) 1} @@ -309,6 +315,13 @@ instance [Finite ι] : DiscreteTopology (span ℤ (Set.range b)) := by instance [Finite ι] : DiscreteTopology (span ℤ (Set.range b)).toAddSubgroup := inferInstanceAs <| DiscreteTopology (span ℤ (Set.range b)) +theorem setFinite_inter [ProperSpace E] [Finite ι] {s : Set E} (hs : Bornology.IsBounded s) : + Set.Finite (s ∩ span ℤ (Set.range b)) := by + have : DiscreteTopology (span ℤ (Set.range b)) := inferInstance + refine Metric.finite_isBounded_inter_isClosed hs ?_ + change IsClosed (span ℤ (Set.range b)).toAddSubgroup + infer_instance + @[measurability] theorem fundamentalDomain_measurableSet [MeasurableSpace E] [OpensMeasurableSpace E] [Finite ι] : MeasurableSet (fundamentalDomain b) := by diff --git a/Mathlib/Analysis/BoxIntegral/UnitPartition.lean b/Mathlib/Analysis/BoxIntegral/UnitPartition.lean index 092ae83e8c61f3..9c0e70ce750756 100644 --- a/Mathlib/Analysis/BoxIntegral/UnitPartition.lean +++ b/Mathlib/Analysis/BoxIntegral/UnitPartition.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Xavier Roblot. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Xavier Roblot -/ +import Mathlib.Algebra.Module.ZLattice.Basic +import Mathlib.Analysis.BoxIntegral.Integrability import Mathlib.Analysis.BoxIntegral.Partition.Measure import Mathlib.Analysis.BoxIntegral.Partition.Tagged @@ -11,13 +13,12 @@ import Mathlib.Analysis.BoxIntegral.Partition.Tagged Fix `n` a positive integer. `BoxIntegral.unitPartition.box` are boxes in `ι → ℝ` obtained by dividing the unit box uniformly into boxes of side length `1 / n` and translating the boxes by -the lattice `ι → ℤ` so that they cover the whole space. For fixed `n`, there are indexed by vectors `ν : ι → ℤ`. Let `B` be a `BoxIntegral`. A `unitPartition.box` is admissible for `B` (more precisely its index is admissible) if it is contained in `B`. There are finitely many admissible `unitPartition.box` for `B` and thus we can form the corresponing tagged prepartition, see -`BoxIntegral.unitPartition.prepartition` (note that each `unitPartition.Box` comes with its +`BoxIntegral.unitPartition.prepartition` (note that each `unitPartition.box` comes with its tag situated at its "upper most" vertex). If `B` satisfies `hasIntegralVertices`, that is its vertices are in `ι → ℤ`, then the corresponding prepartition is actually a partition. @@ -35,6 +36,20 @@ coordinates in `ℤ` * `BoxIntegral.unitPartition.prepartition_isPartition`: For `B : BoxIntegral.Box`, if `B` has integral vertices, then the prepartition of `unitPartition.box` admissible for `B` is a partition of `B`. + +* `tendsto_tsum_div_pow_atTop_integral`: let `s` be a bounded, measurable set of `ι → ℝ` +whose frontier has zero volume and let `F` be a continuous function. Then the limit as `n → ∞` +of `∑ F x / n ^ card ι`, where the sum is over the points in `s ∩ n⁻¹ • (ι → ℤ)`, tends to the +integral of `F` over `s`. + +* `tendsto_card_div_pow_atTop_volume`: let `s` be a bounded, measurable set of `ι → ℝ` whose +frontier has zero volume. Then the limit as `n → ∞` of `card (s ∩ n⁻¹ • (ι → ℤ)) / n ^ card ι` +tends to the volume of `s`. + +* `tendsto_card_div_pow_atTop_volume'`: a version of `tendsto_card_div_pow_atTop_volume` where we +assume in addition that `x • s ⊆ y • s` whenever `0 < x ≤ y`. Then we get the same limit +`card (s ∩ x⁻¹ • (ι → ℤ)) / x ^ card ι → volume s` but the limit is over a real variable `x`. + -/ noncomputable section @@ -186,7 +201,7 @@ theorem setFinite_index {s : Set (ι → ℝ)} (hs₁ : NullMeasurableSet s) (hs (by simp only [Set.iUnion_subset_iff, Set.inter_subset_right, implies_true]) hs₂ · rw [Set.mem_setOf, Set.inter_eq_self_of_subset_left hν, volume_box] -/-- For `B : BoxIntegral.Box`, the set of indices of `unitPartition.Box` that are subsets of `B`. +/-- For `B : BoxIntegral.Box`, the set of indices of `unitPartition.box` that are subsets of `B`. This is a finite set. These boxes cover `B` if it has integral vertices, see `unitPartition.prepartition_isPartition`. -/ def admissibleIndex (B : Box ι) : Finset (ι → ℤ) := by @@ -293,4 +308,180 @@ theorem prepartition_isPartition {B : Box ι} (hB : hasIntegralVertices B) : rw [TaggedPrepartition.mem_toPrepartition, mem_prepartition_iff] exact ⟨index n x, mem_admissibleIndex_of_mem_box n hB hx, rfl⟩ +open Submodule Pointwise BigOperators + +open scoped Pointwise + +variable (c : ℝ) (s : Set (ι → ℝ)) (F : (ι → ℝ) → ℝ) + +-- The image of `ι → ℤ` inside `ι → ℝ` +local notation "L" => span ℤ (Set.range (Pi.basisFun ℝ ι)) + +variable {n} in +theorem mem_smul_span_iff {v : ι → ℝ} : + v ∈ (n : ℝ)⁻¹ • L ↔ ∀ i, n * v i ∈ Set.range (algebraMap ℤ ℝ) := by + rw [ZSpan.smul _ (inv_ne_zero (NeZero.ne _)), Basis.mem_span_iff_repr_mem] + simp_rw [Basis.repr_isUnitSMul, Pi.basisFun_repr, Units.smul_def, Units.val_inv_eq_inv_val, + IsUnit.unit_spec, inv_inv, smul_eq_mul] + +theorem tag_mem_smul_span (ν : ι → ℤ) : + tag n ν ∈ (n : ℝ)⁻¹ • L := by + refine mem_smul_span_iff.mpr fun i ↦ ⟨ν i + 1, ?_⟩ + rw [tag_apply, div_eq_inv_mul, ← mul_assoc, mul_inv_cancel_of_invertible, one_mul, map_add, + map_one, eq_intCast] + +theorem tag_index_eq_self_of_mem_smul_span {x : ι → ℝ} (hx : x ∈ (n : ℝ)⁻¹ • L) : + tag n (index n x) = x := by + rw [mem_smul_span_iff] at hx + ext i + obtain ⟨a, ha⟩ : ∃ a : ℤ, a = n * x i := hx i + rwa [tag_apply, index_apply, Int.cast_sub, Int.cast_one, sub_add_cancel, ← ha, Int.ceil_intCast, + div_eq_iff (NeZero.ne _), mul_comm] + +theorem eq_of_mem_smul_span_of_index_eq_index {x y : ι → ℝ} (hx : x ∈ (n : ℝ)⁻¹ • L) + (hy : y ∈ (n : ℝ)⁻¹ • L) (h : index n x = index n y) : x = y := by + rw [← tag_index_eq_self_of_mem_smul_span n hx, ← tag_index_eq_self_of_mem_smul_span n hy, h] + +theorem integralSum_eq_tsum_div {B : Box ι} (hB : hasIntegralVertices B) (hs₀ : s ≤ B) : + integralSum (Set.indicator s F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) + (prepartition n B) = (∑' x : ↑(s ∩ (n : ℝ)⁻¹ • L), F x) / n ^ card ι := by + classical + unfold integralSum + have : Fintype ↑(s ∩ (n : ℝ)⁻¹ • L) := by + apply Set.Finite.fintype + rw [← coe_pointwise_smul, ZSpan.smul _ (inv_ne_zero (NeZero.ne _))] + exact ZSpan.setFinite_inter _ (B.isBounded.subset hs₀) + rw [tsum_fintype, Finset.sum_set_coe, Finset.sum_div, eq_comm] + simp_rw [Set.indicator_apply, apply_ite, BoxAdditiveMap.toSMul_apply, Measure.toBoxAdditive_apply, + smul_eq_mul, mul_zero, Finset.sum_ite, Finset.sum_const_zero, add_zero] + refine Finset.sum_bij (fun x _ ↦ box n (index n x)) (fun _ hx ↦ Finset.mem_filter.mpr ?_) + (fun _ hx _ hy h ↦ ?_) (fun I hI ↦ ?_) (fun _ hx ↦ ?_) + · rw [Set.mem_toFinset] at hx + refine ⟨mem_prepartition_boxes_iff.mpr + ⟨index n _, mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1), rfl⟩, ?_⟩ + simp_rw [prepartition_tag n (mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1)), + tag_index_eq_self_of_mem_smul_span n hx.2, hx.1] + · rw [Set.mem_toFinset] at hx hy + exact eq_of_mem_smul_span_of_index_eq_index n hx.2 hy.2 (box_injective n h) + · rw [Finset.mem_filter] at hI + refine ⟨(prepartition n B).tag I, Set.mem_toFinset.mpr ⟨hI.2, ?_⟩, box_index_tag_eq_self n hI.1⟩ + rw [← box_index_tag_eq_self n hI.1, prepartition_tag n + (mem_admissibleIndex_of_mem_box n hB (hs₀ hI.2))] + exact tag_mem_smul_span _ _ + · rw [Set.mem_toFinset] at hx + rw [volume_box, prepartition_tag n (mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1)), + tag_index_eq_self_of_mem_smul_span n hx.2, ENNReal.toReal_div, + ENNReal.one_toReal, ENNReal.toReal_pow, ENNReal.toReal_nat, mul_comm_div, one_mul] + +open Filter + +/-- Let `s` be a bounded, measurable set of `ι → ℝ` whose frontier has zero volume and let `F` +be a continuous function. Then the limit as `n → ∞` of `∑ F x / n ^ card ι`, where the sum is +over the points in `s ∩ n⁻¹ • (ι → ℤ)`, tends to the integral of `F` over `s`. -/ +theorem _root_.tendsto_tsum_div_pow_atTop_integral (hF : Continuous F) (hs₁ : IsBounded s) + (hs₂ : MeasurableSet s) (hs₃ : volume (frontier s) = 0) : + Tendsto (fun n : ℕ ↦ (∑' x : ↑(s ∩ (n : ℝ)⁻¹ • L), F x) / n ^ card ι) + atTop (nhds (∫ x in s, F x)) := by + obtain ⟨B, hB, hs₀⟩ := le_hasIntegralVertices_of_isBounded hs₁ + refine Metric.tendsto_atTop.mpr fun ε hε ↦ ?_ + have h₁ : ∃ C, ∀ x ∈ Box.Icc B, ‖Set.indicator s F x‖ ≤ C := by + obtain ⟨C₀, h₀⟩ := (Box.isCompact_Icc B).exists_bound_of_continuousOn hF.continuousOn + refine ⟨max 0 C₀, fun x hx ↦ ?_⟩ + rw [Set.indicator] + split_ifs with hs + · exact le_max_of_le_right (h₀ x hx) + · exact norm_zero.trans_le <|le_max_left 0 _ + have h₂ : ∀ᵐ x, ContinuousAt (s.indicator F) x := by + filter_upwards [compl_mem_ae_iff.mpr hs₃] with _ h + using (hF.continuousOn).continuousAt_indicator h + obtain ⟨r, hr₁, hr₂⟩ := (hasIntegral_iff.mp <| + AEContinuous.hasBoxIntegral (volume : Measure (ι → ℝ)) h₁ h₂ + IntegrationParams.Riemann) (ε / 2) (half_pos hε) + refine ⟨⌈(r 0 0 : ℝ)⁻¹⌉₊, fun n hn ↦ lt_of_le_of_lt ?_ (half_lt_self_iff.mpr hε)⟩ + have : NeZero n := + ⟨Nat.ne_zero_iff_zero_lt.mpr <| (Nat.ceil_pos.mpr (inv_pos.mpr (r 0 0).prop)).trans_le hn⟩ + rw [← integralSum_eq_tsum_div _ s F hB hs₀, ← Measure.restrict_restrict_of_subset hs₀, + ← integral_indicator hs₂] + refine hr₂ 0 _ ⟨?_, fun _ ↦ ?_, fun h ↦ ?_, fun h ↦ ?_⟩ (prepartition_isPartition _ hB) + · rw [show r 0 = fun _ ↦ r 0 0 from funext_iff.mpr (hr₁ 0 rfl)] + apply prepartition_isSubordinate n B + rw [one_div, inv_le_comm₀ (mod_cast (Nat.pos_of_neZero n)) (r 0 0).prop] + exact le_trans (Nat.le_ceil _) (Nat.cast_le.mpr hn) + · exact prepartition_isHenstock n B + · simp only [IntegrationParams.Riemann, Bool.false_eq_true] at h + · simp only [IntegrationParams.Riemann, Bool.false_eq_true] at h + +/-- Let `s` be a bounded, measurable set of `ι → ℝ` whose frontier has zero volume. Then the limit +as `n → ∞` of `card (s ∩ n⁻¹ • (ι → ℤ)) / n ^ card ι` tends to the volume of `s`. This is a +special case of `tendsto_card_div_pow` with `F = 1`. -/ +theorem _root_.tendsto_card_div_pow_atTop_volume (hs₁ : IsBounded s) + (hs₂ : MeasurableSet s) (hs₃ : volume (frontier s) = 0) : + Tendsto (fun n : ℕ ↦ (Nat.card ↑(s ∩ (n : ℝ)⁻¹ • L) : ℝ) / n ^ card ι) + atTop (nhds (volume s).toReal) := by + convert tendsto_tsum_div_pow_atTop_integral s (fun _ ↦ 1) continuous_const hs₁ hs₂ hs₃ + · rw [tsum_const, nsmul_eq_mul, mul_one, Nat.cast_inj] + · rw [setIntegral_const, smul_eq_mul, mul_one] + +private def tendsto_card_div_pow₁ {c : ℝ} (hc : c ≠ 0) : + ↑(s ∩ c⁻¹ • L) ≃ ↑(c • s ∩ L) := + Equiv.subtypeEquiv (Equiv.smulRight hc) (fun x ↦ by + simp_rw [Set.mem_inter_iff, Equiv.smulRight_apply, Set.smul_mem_smul_set_iff₀ hc, + ← Set.mem_inv_smul_set_iff₀ hc]) + +private theorem tendsto_card_div_pow₂ (hs₁ : IsBounded s) + (hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s) {x y : ℝ} (hx : 0 < x) (hy : x ≤ y) : + Nat.card ↑(s ∩ x⁻¹ • L) ≤ Nat.card ↑(s ∩ y⁻¹ • L) := by + rw [Nat.card_congr (tendsto_card_div_pow₁ s hx.ne'), + Nat.card_congr (tendsto_card_div_pow₁ s (hx.trans_le hy).ne')] + refine Nat.card_mono ?_ ?_ + · exact ZSpan.setFinite_inter _ (IsBounded.smul₀ hs₁ y) + · exact Set.inter_subset_inter_left _ <| hs₄ hx hy + +private theorem tendsto_card_div_pow₃ (hs₁ : IsBounded s) + (hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s) : + ∀ᶠ x : ℝ in atTop, (Nat.card ↑(s ∩ (⌊x⌋₊ : ℝ)⁻¹ • L) : ℝ) / x ^ card ι ≤ + (Nat.card ↑(s ∩ x⁻¹ • L) : ℝ) / x ^ card ι := by + filter_upwards [eventually_ge_atTop 1] with x hx + gcongr + exact tendsto_card_div_pow₂ s hs₁ hs₄ (Nat.cast_pos.mpr (Nat.floor_pos.mpr hx)) + (Nat.floor_le (zero_le_one.trans hx)) + +private theorem tendsto_card_div_pow₄ (hs₁ : IsBounded s) + (hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s) : + ∀ᶠ x : ℝ in atTop, (Nat.card ↑(s ∩ x⁻¹ • L) : ℝ) / x ^ card ι ≤ + (Nat.card ↑(s ∩ (⌈x⌉₊ : ℝ)⁻¹ • L) : ℝ) / x ^ card ι := by + filter_upwards [eventually_gt_atTop 0] with x hx + gcongr + exact tendsto_card_div_pow₂ s hs₁ hs₄ hx (Nat.le_ceil _) + +private theorem tendsto_card_div_pow₅ : + (fun x ↦ (Nat.card ↑(s ∩ (⌊x⌋₊ : ℝ)⁻¹ • L) : ℝ) / ⌊x⌋₊ ^ card ι * (⌊x⌋₊ / x) ^ card ι) + =ᶠ[atTop] (fun x ↦ (Nat.card ↑(s ∩ (⌊x⌋₊ : ℝ)⁻¹ • L) : ℝ) / x ^ card ι) := by + filter_upwards [eventually_ge_atTop 1] with x hx + have : 0 < ⌊x⌋₊ := Nat.floor_pos.mpr hx + rw [div_pow, mul_div, div_mul_cancel₀ _ (by positivity)] + +private theorem tendsto_card_div_pow₆ : + (fun x ↦ (Nat.card ↑(s ∩ (⌈x⌉₊ : ℝ)⁻¹ • L) : ℝ) / ⌈x⌉₊ ^ card ι * (⌈x⌉₊ / x) ^ card ι) + =ᶠ[atTop] (fun x ↦ (Nat.card ↑(s ∩ (⌈x⌉₊ : ℝ)⁻¹ • L) : ℝ) / x ^ card ι) := by + filter_upwards [eventually_ge_atTop 1] with x hx + have : 0 < ⌊x⌋₊ := Nat.floor_pos.mpr hx + rw [div_pow, mul_div, div_mul_cancel₀ _ (by positivity)] + +/-- A version of `tendsto_card_div_pow_atTop_volume` for a real variable. -/ +theorem _root_.tendsto_card_div_pow_atTop_volume' (hs₁ : IsBounded s) + (hs₂ : MeasurableSet s) (hs₃ : volume (frontier s) = 0) + (hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s) : + Tendsto (fun x : ℝ ↦ (Nat.card ↑(s ∩ x⁻¹ • L) : ℝ) / x ^ card ι) + atTop (nhds (volume s).toReal) := by + rw [show (volume s).toReal = (volume s).toReal * 1 ^ card ι by ring] + refine tendsto_of_tendsto_of_tendsto_of_le_of_le' ?_ ?_ + (tendsto_card_div_pow₃ s hs₁ hs₄) (tendsto_card_div_pow₄ s hs₁ hs₄) + · refine Tendsto.congr' (tendsto_card_div_pow₅ s) (Tendsto.mul ?_ (Tendsto.pow ?_ _)) + · exact Tendsto.comp (tendsto_card_div_pow_atTop_volume s hs₁ hs₂ hs₃) tendsto_nat_floor_atTop + · exact tendsto_nat_floor_div_atTop + · refine Tendsto.congr' (tendsto_card_div_pow₆ s) (Tendsto.mul ?_ (Tendsto.pow ?_ _)) + · exact Tendsto.comp (tendsto_card_div_pow_atTop_volume s hs₁ hs₂ hs₃) tendsto_nat_ceil_atTop + · exact tendsto_nat_ceil_div_atTop + end BoxIntegral.unitPartition diff --git a/Mathlib/LinearAlgebra/Basis/Basic.lean b/Mathlib/LinearAlgebra/Basis/Basic.lean index e3322e7d5c035c..662046a8624b8b 100644 --- a/Mathlib/LinearAlgebra/Basis/Basic.lean +++ b/Mathlib/LinearAlgebra/Basis/Basic.lean @@ -359,6 +359,10 @@ theorem isUnitSMul_apply {v : Basis ι R M} {w : ι → R} (hw : ∀ i, IsUnit ( v.isUnitSMul hw i = w i • v i := unitsSMul_apply i +theorem repr_isUnitSMul {v : Basis ι R₂ M} {w : ι → R₂} (hw : ∀ i, IsUnit (w i)) (x : M) (i : ι) : + (v.isUnitSMul hw).repr x i = (hw i).unit⁻¹ • v.repr x i := + repr_unitsSMul _ _ _ _ + section Fin /-- Let `b` be a basis for a submodule `N` of `M`. If `y : M` is linear independent of `N` diff --git a/Mathlib/Topology/ContinuousOn.lean b/Mathlib/Topology/ContinuousOn.lean index 3e1d97b1dedd03..d65b86c859fa05 100644 --- a/Mathlib/Topology/ContinuousOn.lean +++ b/Mathlib/Topology/ContinuousOn.lean @@ -1416,6 +1416,18 @@ protected lemma Continuous.mulIndicator (hs : ∀ a ∈ frontier s, f a = 1) (hf Continuous (mulIndicator s f) := by classical exact hf.piecewise hs continuous_const +@[to_additive] +theorem ContinuousOn.continuousAt_mulIndicator (hf : ContinuousOn f (interior s)) {x : α} + (hx : x ∉ frontier s) : + ContinuousAt (s.mulIndicator f) x := by + rw [← Set.mem_compl_iff, compl_frontier_eq_union_interior] at hx + obtain h | h := hx + · have hs : interior s ∈ 𝓝 x := mem_interior_iff_mem_nhds.mp (by rwa [interior_interior]) + exact ContinuousAt.congr (hf.continuousAt hs) <| Filter.eventuallyEq_iff_exists_mem.mpr + ⟨interior s, hs, Set.eqOn_mulIndicator.symm.mono interior_subset⟩ + · exact ContinuousAt.congr continuousAt_const <| Filter.eventuallyEq_iff_exists_mem.mpr + ⟨sᶜ, mem_interior_iff_mem_nhds.mp h, Set.eqOn_mulIndicator'.symm⟩ + end Indicator theorem IsOpen.ite' (hs : IsOpen s) (hs' : IsOpen s')