Exact source: MathlibAnnex/Analysis/Normed/Plucker/Average.lean
Pinned GitHub source · Raw UTF-8 source
Back to The average of contractive derivative generators lies in the body · Back to One boundary extension with all five analytic properties
1import MathlibAnnex.Analysis.Convex.PluckerBody2import MathlibAnnex.Analysis.Calculus.FDeriv.SeminormBound3import Mathlib.Analysis.Convex.Integral45/-!6# Derivative generators and their average78The generator uses the original Lebesgue ball volume and increasing-row maximal9minors. Averaging over the same closed ball preserves membership in the convex10body. All statements include dimension zero and empty maximal-minor index sets.11-/1213noncomputable section1415open Set MeasureTheory16open scoped BigOperators ENNReal1718namespace MathlibAnnex.Plucker1920/-- The volume-scaled maximal-minor vector of a Fréchet derivative. -/21def derivativeGenerator {n N : ℕ} (M : EquivalentSeminorm (Fin n → ℝ))22 (f : (Fin n → ℝ) → (Fin N → ℝ)) (x : Fin n → ℝ) :23 Matrix.MaximalMinorIndex n (Fin N) → ℝ :=24 Matrix.ballVolumeScaledMaximalMinors M (fderiv ℝ f x)2526/-- The set average of derivative generators over the model closed unit ball. -/27def derivativeAverage {n N : ℕ} (M : EquivalentSeminorm (Fin n → ℝ))28 (f : (Fin n → ℝ) → (Fin N → ℝ)) :29 Matrix.MaximalMinorIndex n (Fin N) → ℝ :=30 ⨍ x in M.closedUnitBall, derivativeGenerator M f x ∂volume3132/-- A contractive derivative is a positive raw generator. -/33theorem derivativeGenerator_mem_raw {n N : ℕ} (M : EquivalentSeminorm (Fin n → ℝ))34 (f : (Fin n → ℝ) → (Fin N → ℝ)) {x : Fin n → ℝ}35 (hx : M.IsContraction (fderiv ℝ f x)) :36 derivativeGenerator M f x ∈ PluckerBody.generators M N := by37 exact ⟨fderiv ℝ f x, hx, Or.inl rfl⟩3839/-- The average of integrable, almost everywhere contractive derivative40generators belongs to the model Plücker body. -/41theorem derivativeAverage_mem_body {n N : ℕ} (M : EquivalentSeminorm (Fin n → ℝ))42 {f : (Fin n → ℝ) → (Fin N → ℝ)}43 (hcontract : ∀ᵐ x ∂volume.restrict M.closedUnitBall,44 M.IsContraction (fderiv ℝ f x))45 (hint : IntegrableOn (derivativeGenerator M f) M.closedUnitBall volume) :46 derivativeAverage M f ∈ PluckerBody.body M N := by47 have hzero : volume M.closedUnitBall ≠ 0 := by48 intro h49 have hp := M.closedUnitBallVolume_pos50 simp [EquivalentSeminorm.closedUnitBallVolume, h] at hp51 apply (convex_convexHull ℝ (PluckerBody.generators M N)).set_average_mem52 (isCompact_convexHull_pi _ (PluckerBody.isCompact_generators M)).isClosed53 hzero M.isCompact_closedUnitBall.measure_ne_top54 · filter_upwards [hcontract] with x hx55 exact subset_convexHull ℝ _ (derivativeGenerator_mem_raw M f hx)56 · exact hint5758/-- A global seminorm increment bound gives integrability on the model ball. -/59theorem integrableOn_derivativeGenerator_of_seminormLipschitz {n N : ℕ}60 (M : EquivalentSeminorm (Fin n → ℝ)) {f : (Fin n → ℝ) → (Fin N → ℝ)}61 (hf : ∀ x y, ‖f x - f y‖ ≤ M.p (x - y)) :62 IntegrableOn (derivativeGenerator M f) M.closedUnitBall volume := by63 have hmeas : StronglyMeasurable (derivativeGenerator M f) :=64 ((Matrix.continuous_ballVolumeScaledMaximalMinors M).measurable.comp65 (measurable_fderiv ℝ f)).stronglyMeasurable66 have hcontract : ∀ᵐ x ∂volume.restrict M.closedUnitBall,67 M.IsContraction (fderiv ℝ f x) :=68 FDeriv.ae_norm_apply_le_seminorm_of_lipschitz M.p69 ⟨M.upper, M.upper_pos.le⟩ M.le_upper hf M.closedUnitBall70 rcases (PluckerBody.isCompact_generators (N := N) M).isBounded.subset_closedBall71 (0 : Matrix.MaximalMinorIndex n (Fin N) → ℝ) with ⟨C, hC⟩72 have hnorm : ∀ᵐ x ∂volume.restrict M.closedUnitBall,73 ‖derivativeGenerator M f x‖ ≤ max C 0 := by74 filter_upwards [hcontract] with x hx75 have hfxC : ‖derivativeGenerator M f x‖ ≤ C := by76 simpa only [Metric.mem_closedBall, dist_zero_right] using77 hC (derivativeGenerator_mem_raw M f hx)78 exact hfxC.trans (le_max_left _ _)79 exact IntegrableOn.of_bound80 (lt_top_iff_ne_top.mpr M.isCompact_closedUnitBall.measure_ne_top)81 hmeas.aestronglyMeasurable (max C 0) hnorm8283/-- An ordinary Lipschitz map has integrable derivative generators on every84compact subset of its finite-dimensional source. -/85theorem integrableOn_derivativeGenerator_compact {n N : ℕ}86 (M : EquivalentSeminorm (Fin n → ℝ)) {f : (Fin n → ℝ) → (Fin N → ℝ)}87 (hf : ∃ C : NNReal, LipschitzWith C f) {K : Set (Fin n → ℝ)} (hK : IsCompact K) :88 IntegrableOn (derivativeGenerator M f) K volume := by89 rcases hf with ⟨C, hC⟩90 let D : Set ((Fin n → ℝ) →L[ℝ] (Fin N → ℝ)) := Metric.closedBall 0 (C : ℝ)91 have hD : IsCompact D := by92 simpa [D] using93 (isCompact_closedBall (0 : (Fin n → ℝ) →L[ℝ] (Fin N → ℝ)) (C : ℝ))94 have hP : IsCompact (Matrix.ballVolumeScaledMaximalMinors M '' D) :=95 hD.image (Matrix.continuous_ballVolumeScaledMaximalMinors M)96 have hmeas : StronglyMeasurable (derivativeGenerator M f) :=97 ((Matrix.continuous_ballVolumeScaledMaximalMinors M).measurable.comp98 (measurable_fderiv ℝ f)).stronglyMeasurable99 have hmem : ∀ᵐ x ∂volume.restrict K,100 derivativeGenerator M f x ∈ Matrix.ballVolumeScaledMaximalMinors M '' D :=101 Filter.Eventually.of_forall fun x => by102 refine ⟨fderiv ℝ f x, ?_, rfl⟩103 change fderiv ℝ f x ∈ Metric.closedBall 0 (C : ℝ)104 rw [Metric.mem_closedBall]105 simpa [dist_zero_right] using (norm_fderiv_le_of_lipschitz ℝ hC (x₀ := x))106 rcases hP.isBounded.subset_closedBall107 (0 : Matrix.MaximalMinorIndex n (Fin N) → ℝ) with ⟨B, hB⟩108 have hnorm : ∀ᵐ x ∂volume.restrict K, ‖derivativeGenerator M f x‖ ≤ max B 0 := by109 filter_upwards [hmem] with x hx110 have hfxB : ‖derivativeGenerator M f x‖ ≤ B := by111 simpa only [Metric.mem_closedBall, dist_zero_right] using hB hx112 exact hfxB.trans (le_max_left _ _)113 exact IntegrableOn.of_bound (lt_top_iff_ne_top.mpr hK.measure_ne_top)114 hmeas.aestronglyMeasurable (max B 0) hnorm115116end MathlibAnnex.Plucker