Exact source: MathlibAnnex/MeasureTheory/Integral/MaximalMinor.lean
Pinned GitHub source · Raw UTF-8 source
Back to Weak Piola identity for a compactly supported test field · Back to Maximal-minor integral differences for Lipschitz perturbations
1import MathlibAnnex.Analysis.Calculus.Piola2import MathlibAnnex.Analysis.Calculus.Mollification3import MathlibAnnex.Analysis.Normed.Operator.SelectedMinor4import MathlibAnnex.MeasureTheory.Integral.DeterminantContinuity56/-! # Integrals of maximal minors under compact perturbations -/7noncomputable section8open Set MeasureTheory Filter9open scoped BigOperators Topology ENNReal NNReal10namespace MathlibAnnex11namespace NullLagrangian12open Mollification1314/-- A selected maximal minor of the derivative, using the fixed increasing row order. -/15def maximalMinorIntegrand {n N : ℕ} (s : Matrix.MaximalMinorIndex n (Fin N))16 (f : (Fin n → ℝ) → (Fin N → ℝ)) (x : Fin n → ℝ) : ℝ :=17 LinearMap.det ((ContinuousLinearMap.selectedSquare s (fderiv ℝ f x)).toLinearMap)1819theorem hasCompactSupport_selectedOutput20 {n N : ℕ} (s : Matrix.MaximalMinorIndex n (Fin N)) {u : (Fin n → ℝ) → (Fin N → ℝ)}21 (huc : HasCompactSupport u) :22 HasCompactSupport (fun x => ContinuousLinearMap.selectedOutput s (u x)) :=23 by2425 have hs : Function.support (fun x => ContinuousLinearMap.selectedOutput s (u x)) ⊆26 Function.support u := by27 intro x hx hux28 exact hx (by simp [hux])29 unfold HasCompactSupport at huc ⊢30 exact huc.of_isClosed_subset isClosed_closure (closure_mono hs)3132theorem integral_maximalMinor_fderiv_add_sub_eq_zero_of_contDiff33 {m N : ℕ} (s : Matrix.MaximalMinorIndex (m + 1) (Fin N))34 {g u : (Fin (m + 1) → ℝ) → (Fin N → ℝ)}35 (hg : ContDiff ℝ (↑(⊤ : ℕ∞)) g) (hu : ContDiff ℝ (↑(⊤ : ℕ∞)) u)36 (huc : HasCompactSupport u) :37 ∫ x, (maximalMinorIntegrand s (fun y => g y + u y) x -38 maximalMinorIntegrand s g x) = 0 :=39 by40 let π := ContinuousLinearMap.selectedOutput s41 have hgc : ContDiff ℝ (↑(⊤ : ℕ∞)) (fun x => π (g x)) := π.contDiff.comp hg42 have hucd : ContDiff ℝ (↑(⊤ : ℕ∞)) (fun x => π (u x)) := π.contDiff.comp hu43 have hucs : HasCompactSupport (fun x => π (u x)) :=44 hasCompactSupport_selectedOutput s huc45 have hsq := Piola.integral_det_fderiv_add_sub_eq_zero_of_contDiff hgc hucd hucs4647 have hsum : (fun y => π (g y) + π (u y)) =48 (fun y => π (g y + u y)) := by49 funext y50 exact (map_add π (g y) (u y)).symm51 rw [hsum] at hsq52 have hplus : Differentiable ℝ (fun y => g y + u y) :=53 (hg.differentiable (by simp)).add (hu.differentiable (by simp))54 have hdplus : ∀ x, fderiv ℝ (fun y => π (g y + u y)) x =55 π.comp (fderiv ℝ (fun y => g y + u y) x) := by56 intro x57 exact (π.hasFDerivAt.comp x (hplus x).hasFDerivAt).fderiv58 have hdg : ∀ x, fderiv ℝ (fun y => π (g y)) x =59 π.comp (fderiv ℝ g x) := by60 intro x61 exact (π.hasFDerivAt.comp x62 ((hg.differentiable (by simp)) x).hasFDerivAt).fderiv63 simpa only [maximalMinorIntegrand, ContinuousLinearMap.selectedSquare, hdplus, hdg] using hsq64theorem continuous_maximalMinorIntegrand_mollify {n N : ℕ}65 (s : Matrix.MaximalMinorIndex n (Fin N)) {ε : ℝ} (hε : 0 < ε)66 {f : (Fin n → ℝ) → (Fin N → ℝ)} (hf : LocallyIntegrable f volume) :67 Continuous (maximalMinorIntegrand s (mollify ε f)) := by68 have hD : Continuous (fun x => fderiv ℝ (mollify ε f) x) :=69 (contDiff_mollify hε hf).continuous_fderiv (by simp)70 change Continuous (fun x => LinearMap.det ((ContinuousLinearMap.selectedSquare s71 (fderiv ℝ (mollify ε f) x)).toLinearMap))72 apply ContinuousLinearMap.continuous_det.comp73 convert (ContinuousLinearMap.selectedSquareCLM s).continuous.comp hD using 174 funext x75 exact ContinuousLinearMap.selectedSquareCLM_apply s _767778theorem tendsto_integral_maximalMinor_mollify79 {m N : ℕ} (s : Matrix.MaximalMinorIndex (m + 1) (Fin N))80 {f : (Fin (m + 1) → ℝ) → (Fin N → ℝ)} {C : ℝ≥0}81 (hf : LipschitzWith C f) {K : Set (Fin (m + 1) → ℝ)} (hK : IsCompact K) :82 Tendsto (fun ε => ∫ x in K, maximalMinorIntegrand s (mollify ε f) x)83 (𝓝[>] (0 : ℝ)) (𝓝 (∫ x in K, maximalMinorIntegrand s f x)) := by84 have hstrong := tendsto_eLpNorm_fderiv_mollify_sub hf hK85 have hQ := lipschitz_fderiv_memLpOn_compact hf hK86 apply MathlibAnnex.MeasureTheory.tendsto_integral_det_of_strongLn (Nat.succ_pos m)87 · constructor88 · apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hstrong.189 · intro ε; exact bot_le90 · intro ε91 apply eLpNorm_mono92 intro x93 rw [← ContinuousLinearMap.selectedSquare_sub]94 exact ContinuousLinearMap.norm_selectedSquare_le s _95 · filter_upwards [hstrong.2] with ε hε96 simpa only [ContinuousLinearMap.selectedSquareCLM_apply] using97 hε.continuousLinearMap_comp (ContinuousLinearMap.selectedSquareCLM s)98 · simpa only [ContinuousLinearMap.selectedSquareCLM_apply, Nat.cast_add, Nat.cast_one,99 Nat.cast_succ] using100 hQ.continuousLinearMap_comp (ContinuousLinearMap.selectedSquareCLM s)101102theorem integrableOn_maximalMinor_fderiv_of_lipschitzWith103 {m N : ℕ} (s : Matrix.MaximalMinorIndex (m + 1) (Fin N))104 {f : (Fin (m + 1) → ℝ) → (Fin N → ℝ)} {C : ℝ≥0}105 (hf : LipschitzWith C f) {K : Set (Fin (m + 1) → ℝ)} (hK : IsCompact K) :106 IntegrableOn (maximalMinorIntegrand s f) K := by107 let Q := fun x => ContinuousLinearMap.selectedSquare s (fderiv ℝ f x)108 have hQ : MemLp Q ((m + 1 : ℕ) : ℝ≥0∞) (volume.restrict K) := by109 simpa only [Q, ContinuousLinearMap.selectedSquareCLM_apply, Nat.cast_add, Nat.cast_one] using110 (lipschitz_fderiv_memLpOn_compact hf hK).continuousLinearMap_comp111 (ContinuousLinearMap.selectedSquareCLM s)112 have hzero : LinearMap.det (0 : (Fin (m + 1) → ℝ) →ₗ[ℝ] (Fin (m + 1) → ℝ)) = 0 := by113 rw [← LinearMap.det_toMatrix']114 simpa using (Matrix.det_zero (inferInstance : Nonempty (Fin (m + 1))))115 have hb : ∀ x, ‖LinearMap.det (Q x).toLinearMap‖ ≤ (m + 1 : ℕ) * ‖Q x‖ ^ (m + 1) := by116 intro x117 have h := MathlibAnnex.ContinuousLinearMap.norm_det_sub_le (Q x) 0118 simpa [hzero, pow_succ, mul_assoc] using h119 exact ((hQ.integrable_norm_pow (Nat.succ_ne_zero m)).const_mul (m + 1 : ℕ)).mono'120 (ContinuousLinearMap.continuous_det.comp_aestronglyMeasurable hQ.1)121 (ae_of_all _ hb)122123theorem topMinor_difference_eq_zero_of_not_mem_tsupport124 {n N : ℕ} (s : Matrix.MaximalMinorIndex n (Fin N))125 {g u : (Fin n → ℝ) → (Fin N → ℝ)}126 {x : (Fin n → ℝ)} (hx : x ∉ tsupport u) :127 maximalMinorIntegrand s (fun y => g y + u y) x -128 maximalMinorIntegrand s g x = 0 := by129 have hu0 : u =ᶠ[nhds x] 0 :=130 notMem_tsupport_iff_eventuallyEq.mp hx131 have hsum : (fun y => g y + u y) =ᶠ[nhds x] g := by132 filter_upwards [hu0] with y hy133 simp [hy]134 have hfd : fderiv ℝ (fun y => g y + u y) x = fderiv ℝ g x :=135 hsum.fderiv_eq136 simp [maximalMinorIntegrand, hfd]137138theorem integral_topMinor_difference_eq_setIntegral139 {n N : ℕ} (s : Matrix.MaximalMinorIndex n (Fin N)) {K : Set ((Fin n → ℝ))}140 {g u : (Fin n → ℝ) → (Fin N → ℝ)}141 (hsupp : tsupport u ⊆ K) :142 ∫ x, (maximalMinorIntegrand s (fun y => g y + u y) x -143 maximalMinorIntegrand s g x) =144 ∫ x in K, (maximalMinorIntegrand s (fun y => g y + u y) x -145 maximalMinorIntegrand s g x) := by146 symm147 apply setIntegral_eq_integral_of_forall_compl_eq_zero148 intro x hxK149 exact topMinor_difference_eq_zero_of_not_mem_tsupport s150 (fun hxu => hxK (hsupp hxu))151theorem integral_maximalMinor_fderiv_add_sub_eq_zero_of_lipschitzWith152 {m N : ℕ} (s : Matrix.MaximalMinorIndex (m + 1) (Fin N))153 {g u : (Fin (m + 1) → ℝ) → (Fin N → ℝ)}154 {Cg Cu : ℝ≥0} (hg : LipschitzWith Cg g) (hu : LipschitzWith Cu u) (huc : HasCompactSupport u) :155 ∫ x, (maximalMinorIntegrand s (fun y => g y + u y) x -156 maximalMinorIntegrand s g x) = 0 := by157158 have hgW := hg159 have huW := hu160 have hgL := hgW161 have huL := huW162 have hgLI : LocallyIntegrable g volume := hgW.continuous.locallyIntegrable163 have huLI : LocallyIntegrable u volume := huW.continuous.locallyIntegrable164 rcases eventually_tsupport_mollify_subset_compact huc with165 ⟨K, hK, hsupp_u, hKsupp⟩166 have hplus : LipschitzWith (Cg + Cu) (fun x => g x + u x) := hgW.add huW167 have hsmooth : ∀ᶠ ε in 𝓝[>] (0 : ℝ),168 ∫ x in K, (maximalMinorIntegrand s (mollify ε (fun y => g y + u y)) x -169 maximalMinorIntegrand s (mollify ε g) x) = 0 := by170 filter_upwards [hKsupp, self_mem_nhdsWithin] with ε hsupp hε171 have hε' : 0 < ε := hε172 rw [mollify_add ε g u hgLI huLI]173 rw [← integral_topMinor_difference_eq_setIntegral s hsupp]174 exact integral_maximalMinor_fderiv_add_sub_eq_zero_of_contDiff s175 (contDiff_mollify hε' hgLI)176 (contDiff_mollify hε' huLI)177 (hK.of_isClosed_subset (isClosed_tsupport _) hsupp)178 have hconv_plus := tendsto_integral_maximalMinor_mollify s hplus hK179 have hconv_g := tendsto_integral_maximalMinor_mollify s hgL hK180 have hsplit : ∀ᶠ ε in 𝓝[>] (0 : ℝ),181 (∫ x in K,182 (maximalMinorIntegrand s (mollify ε (fun y => g y + u y)) x -183 maximalMinorIntegrand s (mollify ε g) x)) =184 (∫ x in K, maximalMinorIntegrand s (mollify ε (fun y => g y + u y)) x) -185 ∫ x in K, maximalMinorIntegrand s (mollify ε g) x := by186 filter_upwards [self_mem_nhdsWithin] with ε hε187 have hε' : 0 < ε := hε188 exact MeasureTheory.integral_sub189 (ContinuousOn.integrableOn_compact hK190 (continuous_maximalMinorIntegrand_mollify s hε'191 (hplus.continuous.locallyIntegrable)).continuousOn)192 (ContinuousOn.integrableOn_compact hK193 (continuous_maximalMinorIntegrand_mollify s hε' hgLI).continuousOn)194 have hdiff : Tendsto195 (fun ε => ∫ x in K,196 (maximalMinorIntegrand s (mollify ε (fun y => g y + u y)) x -197 maximalMinorIntegrand s (mollify ε g) x))198 (𝓝[>] (0 : ℝ))199 (𝓝 (∫ x in K,200 (maximalMinorIntegrand s (fun y => g y + u y) x -201 maximalMinorIntegrand s g x))) := by202 have hplusInt := integrableOn_maximalMinor_fderiv_of_lipschitzWith s hplus hK203 have hgInt := integrableOn_maximalMinor_fderiv_of_lipschitzWith s hgL hK204 have hlimit :205 (∫ x in K,206 (maximalMinorIntegrand s (fun y => g y + u y) x -207 maximalMinorIntegrand s g x)) =208 (∫ x in K, maximalMinorIntegrand s (fun y => g y + u y) x) -209 ∫ x in K, maximalMinorIntegrand s g x :=210 MeasureTheory.integral_sub hplusInt hgInt211 rw [hlimit]212 have hsplitEq :213 (fun ε =>214 (∫ x in K,215 (maximalMinorIntegrand s (mollify ε (fun y => g y + u y)) x -216 maximalMinorIntegrand s (mollify ε g) x))) =ᶠ[𝓝[>] (0 : ℝ)]217 (fun ε =>218 (∫ x in K, maximalMinorIntegrand s219 (mollify ε (fun y => g y + u y)) x) -220 ∫ x in K, maximalMinorIntegrand s (mollify ε g) x) := hsplit221 exact (hconv_plus.sub hconv_g).congr' hsplitEq.symm222 have hzero : ∫ x in K,223 (maximalMinorIntegrand s (fun y => g y + u y) x -224 maximalMinorIntegrand s g x) = 0 := by225 have heq :226 (fun ε => ∫ x in K,227 (maximalMinorIntegrand s (mollify ε (fun y => g y + u y)) x -228 maximalMinorIntegrand s (mollify ε g) x)) =ᶠ[𝓝[>] (0 : ℝ)]229 (fun _ => 0) := hsmooth230 have hzlim : Tendsto231 (fun ε => ∫ x in K,232 (maximalMinorIntegrand s (mollify ε (fun y => g y + u y)) x -233 maximalMinorIntegrand s (mollify ε g) x))234 (𝓝[>] (0 : ℝ)) (𝓝 0) :=235 tendsto_const_nhds.congr' heq.symm236 exact tendsto_nhds_unique hdiff hzlim237 rw [integral_topMinor_difference_eq_setIntegral s hsupp_u]238 exact hzero239240241end NullLagrangian242end MathlibAnnex