PL1/FiniteDimensionalRNP.lean

All source files · Download exact source

SHA-256: 5233c277b78cc3674b77126323c52c0da52bd543a9752d26df6145312e0bec91

1import PL1.RNPBridge2import Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym3import Mathlib.MeasureTheory.SpecificCodomains.Pi4import Mathlib.Analysis.Normed.Module.FiniteDimension5import Mathlib.Analysis.RCLike.Lemmas67/-! # Finite-dimensional spaces satisfy the full reviewed RNP -/89noncomputable section10universe u v w11open MeasureTheory Set12open scoped ENNReal MeasureTheory1314namespace PL1.RNPBridge1516/-- Scalar Radon–Nikodym is exactly the reviewed RNP in dimension one. -/17theorem hasRadonNikodymProperty_real : HasRadonNikodymProperty.{0, w} ℝ := by18  intro Ω mΩ19  let := mΩ20  intro μ hμ ν hν hAC21  let : IsFiniteMeasure μ := ⟨hμ⟩22  have ha : ν ≪ᵥ μ.toENNRealVectorMeasure := by23    apply VectorMeasure.AbsolutelyContinuous.mk24    intro A hA hzero25    rw [Measure.toENNRealVectorMeasure_apply_measurable hA] at hzero26    exact hAC A hA hzero27  refine ⟨SignedMeasure.rnDeriv ν μ, SignedMeasure.integrable_rnDeriv ν μ, ?_⟩28  intro A hA29  have h := congrArg (fun s : SignedMeasure Ω => s A)30    (SignedMeasure.withDensityᵥ_rnDeriv_eq ν μ ha)31  rw [withDensityᵥ_apply (SignedMeasure.integrable_rnDeriv ν μ) hA] at h32  exact h.symm3334/-- Finite products of real lines have densities coordinate by coordinate. -/35theorem hasRadonNikodymProperty_real_pi (ι : Type v) [Fintype ι] :36    HasRadonNikodymProperty.{v, w} (ι → ℝ) := by37  classical38  intro Ω mΩ39  let := mΩ40  intro μ hμ ν hν hAC41  let s (i : ι) : VectorMeasure Ω ℝ := mapVectorMeasure (ContinuousLinearMap.proj i) ν42  have hsAC (i : ι) : ∀ A : Set Ω, MeasurableSet A → μ A = 0 → s i A = 0 := by43    intro A hA hz44    change (ν A) i = 045    rw [hAC A hA hz]46    rfl47  have hsvar (i : ι) : (s i).variation univ < ∞ := by48    change (mapVectorMeasure (ContinuousLinearMap.proj i : (ι → ℝ) →L[ℝ] ℝ) ν).variation univ < ∞49    exact mapVectorMeasure_finite_variation _ ν hν50  have hs (i : ι) : ∃ g : Ω → ℝ, Integrable g μ ∧51      ∀ A : Set Ω, MeasurableSet A → s i A = ∫ x in A, g x ∂μ :=52    hasRadonNikodymProperty_real Ω mΩ μ hμ (s i) (hsvar i) (hsAC i)53  choose g hg hrepr using hs54  refine ⟨fun x i => g i x, Integrable.of_eval hg, ?_⟩55  intro A hA56  funext i57  rw [eval_integral (fun j => (hg j).integrableOn)]58  exact hrepr i A hA5960/-- Every finite-dimensional real normed space has the full vector-measure RNP. -/61theorem hasRadonNikodymProperty_of_finiteDimensional62    (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] :63    HasRadonNikodymProperty.{u, w} E := by64  let e := (Module.finBasis ℝ E).equivFun.toContinuousLinearEquiv65  exact hasRadonNikodymProperty_of_equiv e.symm66    (hasRadonNikodymProperty_real_pi (Fin (Module.finrank ℝ E)))6768/-- Failure of the reviewed RNP witnesses infinite real dimension. -/69theorem not_finiteDimensional_of_not_RNP70    (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E]71    (hE : ¬ HasRadonNikodymProperty.{u, w} E) : ¬ FiniteDimensional ℝ E := by72  intro h73  let := h74  exact hE (hasRadonNikodymProperty_of_finiteDimensional E)7576/-- Finite dimension over either scalar field implies real RNP for the explicit77underlying-real space used by the reviewed statements. -/78theorem underlyingReal_hasRNP_of_finiteDimensional79    (𝕜 : Type*) [RCLike 𝕜] (E : Type u) [NormedAddCommGroup E] [NormedSpace 𝕜 E]80    [FiniteDimensional 𝕜 E] :81    @HasRadonNikodymProperty.{u, w} (UnderlyingReal 𝕜 E)82      (inferInstanceAs (NormedAddCommGroup E)) (NormedSpace.restrictScalars ℝ 𝕜 E) := by83  let : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E84  let : FiniteDimensional ℝ E := FiniteDimensional.trans ℝ 𝕜 E85  exact hasRadonNikodymProperty_of_finiteDimensional E8687/-- Failure of underlying-real RNP implies infinite dimension over ℝ or ℂ. -/88theorem not_finiteDimensional_scalar_of_not_RNP89    (𝕜 : Type*) [RCLike 𝕜] (E : Type u) [NormedAddCommGroup E] [NormedSpace 𝕜 E]90    (hE : ¬ @HasRadonNikodymProperty.{u, w} (UnderlyingReal 𝕜 E)91      (inferInstanceAs (NormedAddCommGroup E)) (NormedSpace.restrictScalars ℝ 𝕜 E)) :92    ¬ FiniteDimensional 𝕜 E := by93  intro h94  let := h95  exact hE (underlyingReal_hasRNP_of_finiteDimensional 𝕜 E)9697end PL1.RNPBridge9899100101102