Exact source: MathlibAnnex/MeasureTheory/Integral/DeterminantContinuity.lean
Pinned GitHub source · Raw UTF-8 source
Back to Determinant integrals under strong $L^n$ convergence
1import MathlibAnnex.Analysis.Normed.Operator.Determinant2import Mathlib.MeasureTheory.SpecificCodomains.Pi3import Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp4import Mathlib.MeasureTheory.Function.LpSpace.Basic5import Mathlib.MeasureTheory.Integral.Bochner.Basic6import Mathlib.Topology.Algebra.Module.FiniteDimension7import Mathlib.Tactic89/-!10# Strong L^n continuity of determinant integrals1112The determinant estimate on continuous linear maps yields convergence of13integrals under strong L^n convergence. The source is an arbitrary measure14space; eventual L^n membership of the approximants is part of the hypothesis.15-/1617noncomputable section1819open Set MeasureTheory Filter20open scoped BigOperators ENNReal NNReal Topology2122namespace MathlibAnnex.MeasureTheory2324/-- Qualified strong L^n convergence over an arbitrary measure space. -/25def StrongLnOperatorField {n : ℕ} {α ι : Type*} [MeasurableSpace α]26 (l : Filter ι) (μ : Measure α)27 (P : ι → α → ((Fin n → ℝ) →L[ℝ] (Fin n → ℝ)))28 (Q : α → ((Fin n → ℝ) →L[ℝ] (Fin n → ℝ))) : Prop :=29 Tendsto (fun i => eLpNorm (fun x => P i x - Q x) n μ) l (𝓝 0) ∧30 ∀ᶠ i in l, MemLp (P i) n μ3132/-- Strong L^n convergence of square matrix fields implies convergence of33integrals of their determinants, over an arbitrary measure space. -/34theorem tendsto_integral_det_of_strongLn35 {n : ℕ} (hn : 0 < n) {α ι : Type*} [MeasurableSpace α]36 {l : Filter ι} {μ : Measure α}37 {P : ι → α → ((Fin n → ℝ) →L[ℝ] (Fin n → ℝ))}38 {Q : α → ((Fin n → ℝ) →L[ℝ] (Fin n → ℝ))}39 (hstrong : StrongLnOperatorField l μ P Q)40 (hQ : MemLp Q n μ) :41 Tendsto (fun i => ∫ x,42 LinearMap.det (P i x : (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ)) ∂μ) l43 (𝓝 (∫ x,44 LinearMap.det (Q x : (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ)) ∂μ)) := by45 let det : (((Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) → ℝ) :=46 fun A => LinearMap.det (A : (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ))47 change Tendsto (fun i => ∫ x, det (P i x) ∂μ) l48 (𝓝 (∫ x, det (Q x) ∂μ))49 have hP : ∀ᶠ i in l, MemLp (P i) n μ := hstrong.250 have hdiff : ∀ᶠ i in l, MemLp (fun x => P i x - Q x) n μ := by51 filter_upwards [hP] with i hi52 exact hi.sub hQ53 have hpoint : ∀ i x,54 ‖det (P i x) - det (Q x)‖ ≤55 n * (‖P i x‖ + ‖Q x‖) ^ (n - 1) * ‖P i x - Q x‖ := by56 intro i x57 simpa only [det, Fintype.card_fin] using58 MathlibAnnex.ContinuousLinearMap.norm_det_sub_le (P i x) (Q x)59 have hseminorm : Tendsto60 (fun i => eLpNorm (fun x => P i x - Q x) n μ) l (𝓝 0) :=61 hstrong.162 letI : Nonempty (Fin n) := ⟨⟨0, hn⟩⟩63 have hzero : det (0 : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) = 0 := by64 dsimp [det]65 rw [← LinearMap.det_toMatrix'66 (0 : (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ))]67 simpa using (Matrix.det_zero (inferInstance : Nonempty (Fin n)))68 have hdet_cont : Continuous det := by69 dsimp [det]70 exact ContinuousLinearMap.continuous_det71 (𝕜 := ℝ) (E := (Fin n → ℝ))72 have hdetQ_meas :73 AEStronglyMeasurable (fun x => det (Q x)) μ :=74 hdet_cont.comp_aestronglyMeasurable hQ.175 have hdetQ_bound : ∀ x,76 ‖det (Q x)‖ ≤ (n : ℝ) * ‖Q x‖ ^ n := by77 intro x78 calc79 ‖det (Q x)‖ = ‖det (Q x) - det (0 : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ))‖ := by80 rw [hzero, sub_zero]81 _ ≤ (n : ℝ) * (‖Q x‖ + ‖(0 : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ))‖) ^ (n - 1) *82 ‖Q x - (0 : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ))‖ := by83 simpa only [det, Fintype.card_fin] using84 MathlibAnnex.ContinuousLinearMap.norm_det_sub_le (Q x)85 (0 : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ))86 _ = (n : ℝ) * ‖Q x‖ ^ n := by87 simp only [norm_zero, add_zero, sub_zero]88 rw [mul_assoc, ← pow_succ, Nat.sub_add_cancel hn]89 have hdetQ : Integrable (fun x => det (Q x)) μ := by90 have hdom : Integrable (fun x => (n : ℝ) * ‖Q x‖ ^ n) μ :=91 (hQ.integrable_norm_pow hn.ne').const_mul n92 refine' hdom.mono' hdetQ_meas (ae_of_all μ fun x => _)93 simpa only [Real.norm_eq_abs, abs_of_nonneg (mul_nonneg (Nat.cast_nonneg n)94 (pow_nonneg (norm_nonneg _) n))] using hdetQ_bound x95 by_cases hn1 : n = 196 · subst n97 have hDmem : ∀ᶠ i in l,98 MemLp (fun x => det (P i x) - det (Q x)) 1 μ := by99 filter_upwards [hP, hdiff] with i hi hdi100 have hdi1 : MemLp (fun x => P i x - Q x) 1 μ := by simpa using hdi101 refine' ⟨(hdet_cont.comp_aestronglyMeasurable hi.1).sub102 (hdet_cont.comp_aestronglyMeasurable hQ.1), _⟩103 refine' lt_of_le_of_lt (eLpNorm_mono fun x => _) hdi1.2104 simpa only [Nat.cast_one, one_mul, Nat.sub_self, pow_zero] using hpoint i x105 have hDnorm : Tendsto106 (fun i => eLpNorm (fun x => det (P i x) - det (Q x)) 1 μ)107 l (𝓝 0) := by108 have hseminorm1 : Tendsto109 (fun i => eLpNorm (fun x => P i x - Q x) 1 μ) l (𝓝 0) := by110 simpa using hseminorm111 apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hseminorm1112 · intro i113 exact bot_le114 · intro i115 exact eLpNorm_mono fun x => by116 simpa only [Nat.cast_one, one_mul, Nat.sub_self, pow_zero] using hpoint i x117 have hIntD : Tendsto118 (fun i => ∫ x, det (P i x) - det (Q x) ∂μ) l (𝓝 0) := by119 refine' squeeze_zero_norm'120 (a := fun i => (eLpNorm (fun x => det (P i x) - det (Q x)) 1 μ).toReal)121 _ _122 · filter_upwards [hDmem] with i hi123 refine' (norm_integral_le_integral_norm _).trans_eq _124 have heq := hi.eLpNorm_eq_integral_rpow_norm125 (one_ne_zero : (1 : ℝ≥0∞) ≠ 0) ENNReal.one_ne_top126 have heq' : eLpNorm (fun x => det (P i x) - det (Q x)) 1 μ =127 ENNReal.ofReal (∫ x, ‖det (P i x) - det (Q x)‖ ∂μ) := by128 simpa only [ENNReal.toReal_one, Real.rpow_one, inv_one] using heq129 rw [heq', ENNReal.toReal_ofReal]130 exact integral_nonneg_of_ae (Eventually.of_forall fun x => norm_nonneg _)131 · exact (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp hDnorm132 have hdetP : ∀ᶠ i in l, Integrable (fun x => det (P i x)) μ := by133 filter_upwards [hDmem] with i hi134 have hDi : Integrable (fun x => det (P i x) - det (Q x)) μ :=135 memLp_one_iff_integrable.mp hi136 have hfun : (fun x => det (P i x)) =137 (fun x => det (P i x) - det (Q x)) + (fun x => det (Q x)) := by138 funext x139 exact (sub_add_cancel (det (P i x)) (det (Q x))).symm140 rw [hfun]141 exact hDi.add hdetQ142 change Tendsto (fun i => ∫ x, det (P i x) ∂μ) l143 (𝓝 (∫ x, det (Q x) ∂μ))144 have hconst : Tendsto (fun _ : ι => ∫ x, det (Q x) ∂μ) l145 (𝓝 (∫ x, det (Q x) ∂μ)) := tendsto_const_nhds146 have ht := hconst.add hIntD147 have ht' : Tendsto (fun i => ∫ x, det (P i x) ∂μ) l148 (𝓝 ((∫ x, det (Q x) ∂μ) + 0)) := by149 apply ht.congr'150 filter_upwards [hdetP] with i hi151 rw [integral_sub hi hdetQ]152 ring153 simpa only [add_zero] using ht'154 · have hn2 : 1 < n := by omega155 let p : ℝ≥0∞ := ENNReal.conjExponent n156 letI hnconj : ENNReal.HolderConjugate (n : ℝ≥0∞) p := by157 dsimp [p]158 exact ENNReal.HolderConjugate.conjExponent (by exact_mod_cast hn)159 have hp_mul : p * (n - 1 : ℕ) = (n : ℝ≥0∞) := by160 dsimp [p]161 rw [show ((n - 1 : ℕ) : ℝ≥0∞) = (n : ℝ≥0∞) - 1 by162 simp]163 rw [ENNReal.conjExponent, add_mul, one_mul,164 ENNReal.inv_mul_cancel, tsub_add_cancel_of_le]165 · exact_mod_cast hn166 · exact (tsub_pos_iff_lt.mpr (by exact_mod_cast hn2)).ne'167 · finiteness168 have hbound : ∀ᶠ i in l,169 eLpNorm (fun x => det (P i x) - det (Q x)) 1 μ ≤170 (n : ℝ≥0∞) *171 (eLpNorm (fun x => P i x - Q x) n μ +172 eLpNorm Q n μ + eLpNorm Q n μ) ^ (n - 1) *173 eLpNorm (fun x => P i x - Q x) n μ := by174 filter_upwards [hP, hdiff] with i hi hdi175 let A : α → ℝ := fun x => ‖P i x‖ + ‖Q x‖176 let d : α → ℝ := fun x => ‖P i x - Q x‖177 have hA : MemLp A n μ := by178 dsimp [A]179 exact hi.norm.add hQ.norm180 have hd : MemLp d n μ := by181 dsimp [d]182 exact hdi.norm183 have hpow_meas : AEStronglyMeasurable (fun x => A x ^ (n - 1)) μ :=184 hA.1.pow (n - 1)185 have hpow_norm :186 eLpNorm (fun x => A x ^ (n - 1)) p μ = eLpNorm A n μ ^ (n - 1) := by187 let q : ℝ := (n - 1 : ℕ)188 have hqpos : 0 < q := by189 dsimp [q]190 exact_mod_cast Nat.sub_pos_of_lt hn2191 have hqE : ENNReal.ofReal q = (n - 1 : ℕ) := by192 dsimp [q]193 simp194 have hr := eLpNorm_norm_rpow (μ := μ) (p := p) (q := q) A hqpos195 rw [hqE, hp_mul] at hr196 have hpowfun : (fun x => ‖A x‖ ^ q) = (fun x => A x ^ q) := by197 funext x198 rw [Real.norm_of_nonneg (add_nonneg (norm_nonneg _) (norm_nonneg _))]199 rw [hpowfun] at hr200 simpa only [q, Real.rpow_natCast, ENNReal.rpow_natCast] using hr201 have hholder :202 eLpNorm (fun x => A x ^ (n - 1) * d x) 1 μ ≤203 eLpNorm A n μ ^ (n - 1) * eLpNorm (fun x => P i x - Q x) n μ := by204 calc205 eLpNorm (fun x => A x ^ (n - 1) * d x) 1 μ ≤206 eLpNorm (fun x => A x ^ (n - 1)) p μ * eLpNorm d n μ := by207 have hh := eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm208 (p := p) (q := (n : ℝ≥0∞)) (r := 1) (μ := μ)209 hpow_meas hd.1 (fun a b : ℝ => a * b) 1210 (ae_of_all μ fun x => by211 simpa only [NNReal.coe_one, one_mul] using212 (norm_mul (A x ^ (n - 1)) (d x)).le)213 change eLpNorm (fun x => A x ^ (n - 1) * d x) 1 μ ≤214 (1 : ℝ≥0∞) * eLpNorm (fun x => A x ^ (n - 1)) p μ * eLpNorm d n μ at hh215 simpa only [one_mul] using hh216 _ = eLpNorm A n μ ^ (n - 1) *217 eLpNorm (fun x => P i x - Q x) n μ := by218 rw [hpow_norm]219 simp only [d, eLpNorm_norm]220 have hA_le : eLpNorm A n μ ≤221 eLpNorm (fun x => P i x - Q x) n μ + eLpNorm Q n μ + eLpNorm Q n μ := by222 let B : α → ℝ := fun x => ‖P i x - Q x‖ + ‖Q x‖ + ‖Q x‖223 have hB : MemLp B n μ := by224 dsimp [B]225 exact (hdi.norm.add hQ.norm).add hQ.norm226 calc227 eLpNorm A n μ ≤ eLpNorm B n μ := by228 apply eLpNorm_mono229 intro x230 dsimp [A, B]231 have hp : ‖P i x‖ ≤ ‖P i x - Q x‖ + ‖Q x‖ := by232 calc233 ‖P i x‖ = ‖(P i x - Q x) + Q x‖ := by rw [sub_add_cancel]234 _ ≤ _ := norm_add_le _ _235 have hleft : 0 ≤ ‖P i x‖ + ‖Q x‖ :=236 add_nonneg (norm_nonneg _) (norm_nonneg _)237 have hright : 0 ≤ ‖P i x - Q x‖ + ‖Q x‖ + ‖Q x‖ :=238 add_nonneg (add_nonneg (norm_nonneg _) (norm_nonneg _)) (norm_nonneg _)239 rw [abs_of_nonneg hleft, abs_of_nonneg hright]240 simpa only [add_assoc, add_comm, add_left_comm] using241 (add_le_add_right hp ‖Q x‖)242 _ ≤ eLpNorm (fun x => ‖P i x - Q x‖ + ‖Q x‖) n μ +243 eLpNorm (fun x => ‖Q x‖) n μ := by244 dsimp [B]245 exact eLpNorm_add_le (p := (n : ℝ≥0∞)) (μ := μ)246 (hdi.norm.add hQ.norm).1 hQ.norm.1 (by exact_mod_cast hn)247 _ ≤ (eLpNorm (fun x => ‖P i x - Q x‖) n μ +248 eLpNorm (fun x => ‖Q x‖) n μ) + eLpNorm (fun x => ‖Q x‖) n μ := by249 have htri := eLpNorm_add_le (p := (n : ℝ≥0∞)) (μ := μ)250 hdi.norm.1 hQ.norm.1 (by exact_mod_cast hn)251 calc252 eLpNorm (fun x => ‖P i x - Q x‖ + ‖Q x‖) n μ +253 eLpNorm (fun x => ‖Q x‖) n μ =254 eLpNorm (fun x => ‖Q x‖) n μ +255 eLpNorm (fun x => ‖P i x - Q x‖ + ‖Q x‖) n μ := add_comm _ _256 _ ≤ eLpNorm (fun x => ‖Q x‖) n μ +257 (eLpNorm (fun x => ‖P i x - Q x‖) n μ +258 eLpNorm (fun x => ‖Q x‖) n μ) := add_le_add le_rfl htri259 _ = (eLpNorm (fun x => ‖P i x - Q x‖) n μ +260 eLpNorm (fun x => ‖Q x‖) n μ) +261 eLpNorm (fun x => ‖Q x‖) n μ := by262 simp only [add_comm]263 _ = _ := by simp only [eLpNorm_norm]264 calc265 eLpNorm (fun x => det (P i x) - det (Q x)) 1 μ ≤266 eLpNorm (fun x => (n : ℝ) * (A x ^ (n - 1) * d x)) 1 μ := by267 apply eLpNorm_mono268 intro x269 have hnonneg : 0 ≤ (n : ℝ) * (A x ^ (n - 1) * d x) := by270 exact mul_nonneg (Nat.cast_nonneg n)271 (mul_nonneg272 (pow_nonneg (by273 dsimp [A]274 exact add_nonneg (norm_nonneg _) (norm_nonneg _)) (n - 1))275 (by276 dsimp [d]277 exact norm_nonneg _))278 rw [Real.norm_of_nonneg hnonneg]279 simpa only [A, d, mul_assoc] using hpoint i x280 _ = (n : ℝ≥0∞) * eLpNorm (fun x => A x ^ (n - 1) * d x) 1 μ := by281 have hfun : (fun x => (n : ℝ) * (A x ^ (n - 1) * d x)) =282 n • (fun x => A x ^ (n - 1) * d x) := by283 funext x284 simp [Pi.smul_apply, nsmul_eq_mul]285 rw [hfun]286 exact eLpNorm_nsmul (p := (1 : ℝ≥0∞)) (μ := μ) n287 (fun x => A x ^ (n - 1) * d x)288 _ ≤ (n : ℝ≥0∞) *289 (eLpNorm A n μ ^ (n - 1) * eLpNorm (fun x => P i x - Q x) n μ) := by290 exact mul_le_mul' le_rfl hholder291 _ ≤ (n : ℝ≥0∞) *292 ((eLpNorm (fun x => P i x - Q x) n μ + eLpNorm Q n μ +293 eLpNorm Q n μ) ^ (n - 1) *294 eLpNorm (fun x => P i x - Q x) n μ) := by295 exact mul_le_mul' le_rfl296 (mul_le_mul' (pow_le_pow_left' hA_le (n - 1)) le_rfl)297 _ = _ := by simp only [mul_assoc]298 have hmajor : Tendsto299 (fun i => (n : ℝ≥0∞) *300 (eLpNorm (fun x => P i x - Q x) n μ + eLpNorm Q n μ + eLpNorm Q n μ) ^301 (n - 1) * eLpNorm (fun x => P i x - Q x) n μ)302 l (𝓝 0) := by303 let q : ℝ≥0∞ := eLpNorm Q n μ304 let C : ℝ≥0∞ := (n : ℝ≥0∞) * (1 + q + q) ^ (n - 1)305 have hd_le_one : ∀ᶠ i in l,306 eLpNorm (fun x => P i x - Q x) n μ ≤ 1 := by307 have hlt := (tendsto_order.1 hseminorm).2 (1 : ℝ≥0∞)308 (show (0 : ℝ≥0∞) < 1 from zero_lt_one)309 exact hlt.mono fun i hi => hi.le310 have hC_ne_top : C ≠ ⊤ := by311 dsimp [C, q]312 finiteness [hQ.2]313 have hcontrolled : ∀ᶠ i in l,314 (n : ℝ≥0∞) *315 (eLpNorm (fun x => P i x - Q x) n μ + eLpNorm Q n μ + eLpNorm Q n μ) ^316 (n - 1) * eLpNorm (fun x => P i x - Q x) n μ ≤317 C * eLpNorm (fun x => P i x - Q x) n μ := by318 filter_upwards [hd_le_one] with i hi319 dsimp [C, q]320 exact mul_le_mul'321 (mul_le_mul' le_rfl322 (pow_le_pow_left'323 (add_le_add (add_le_add hi le_rfl) le_rfl) (n - 1)))324 le_rfl325 have hCmul : Tendsto326 (fun i => C * eLpNorm (fun x => P i x - Q x) n μ) l (𝓝 0) := by327 simpa only [mul_zero] using328 ENNReal.Tendsto.const_mul hseminorm (Or.inr hC_ne_top)329 apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hCmul330 · exact Eventually.of_forall fun i => bot_le331 · exact hcontrolled332 have hDnorm : Tendsto333 (fun i => eLpNorm (fun x => det (P i x) - det (Q x)) 1 μ)334 l (𝓝 0) := by335 apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hmajor336 · exact Eventually.of_forall fun i => bot_le337 · exact hbound338 have hDmem : ∀ᶠ i in l,339 MemLp (fun x => det (P i x) - det (Q x)) 1 μ := by340 filter_upwards [hP, hbound, hdiff] with i hi hib hdi341 refine' ⟨(hdet_cont.comp_aestronglyMeasurable hi.1).sub hdetQ_meas, _⟩342 refine' lt_of_le_of_lt hib _343 finiteness [hQ.2, hdi.2]344 have hIntD : Tendsto345 (fun i => ∫ x, det (P i x) - det (Q x) ∂μ) l (𝓝 0) := by346 refine' squeeze_zero_norm'347 (a := fun i => (eLpNorm (fun x => det (P i x) - det (Q x)) 1 μ).toReal)348 _ _349 · filter_upwards [hDmem] with i hi350 refine' (norm_integral_le_integral_norm _).trans_eq _351 have heq := hi.eLpNorm_eq_integral_rpow_norm352 (one_ne_zero : (1 : ℝ≥0∞) ≠ 0) ENNReal.one_ne_top353 have heq' : eLpNorm (fun x => det (P i x) - det (Q x)) 1 μ =354 ENNReal.ofReal (∫ x, ‖det (P i x) - det (Q x)‖ ∂μ) := by355 simpa only [ENNReal.toReal_one, Real.rpow_one, inv_one] using heq356 have hto := congrArg ENNReal.toReal heq'357 have hnonneg : 0 ≤ ∫ x, ‖det (P i x) - det (Q x)‖ ∂μ :=358 integral_nonneg_of_ae (Eventually.of_forall fun x => norm_nonneg _)359 rw [ENNReal.toReal_ofReal hnonneg] at hto360 exact hto.symm361 · exact (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp hDnorm362 have hdetP : ∀ᶠ i in l, Integrable (fun x => det (P i x)) μ := by363 filter_upwards [hDmem] with i hi364 have hDi : Integrable (fun x => det (P i x) - det (Q x)) μ :=365 memLp_one_iff_integrable.mp hi366 have hfun : (fun x => det (P i x)) =367 (fun x => det (P i x) - det (Q x)) + (fun x => det (Q x)) := by368 funext x369 exact (sub_add_cancel (det (P i x)) (det (Q x))).symm370 rw [hfun]371 exact hDi.add hdetQ372 change Tendsto (fun i => ∫ x, det (P i x) ∂μ) l373 (𝓝 (∫ x, det (Q x) ∂μ))374 have hconst : Tendsto (fun _ : ι => ∫ x, det (Q x) ∂μ) l375 (𝓝 (∫ x, det (Q x) ∂μ)) := tendsto_const_nhds376 have ht := hconst.add hIntD377 have ht' : Tendsto (fun i => ∫ x, det (P i x) ∂μ) l378 (𝓝 ((∫ x, det (Q x) ∂μ) + 0)) := by379 apply ht.congr'380 filter_upwards [hdetP] with i hi381 rw [integral_sub hi hdetQ]382 ring383 simpa only [add_zero] using ht'384385end MathlibAnnex.MeasureTheory