PL1/RNPTransport.lean

All source files · Download exact source

SHA-256: 6d003be2b304e803338a39ec89e2ded49dc88deba0fe748f99ae2be47fa87dd3

1import PL1.RNPBridge23/-! # RNP transport with the exact inherited real norm and scalar action -/45noncomputable section6universe u v w7namespace PL1.RNPTransport89variable {𝕜 : Type*} [RCLike 𝕜]10variable {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E]11variable {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F]1213theorem hasRadonNikodymProperty_restrictScalars_iff (e : E ≃L[𝕜] F) :14    @HasRadonNikodymProperty.{u, w} (UnderlyingReal 𝕜 E)15      (inferInstanceAs (NormedAddCommGroup E)) (NormedSpace.restrictScalars ℝ 𝕜 E) ↔16    @HasRadonNikodymProperty.{v, w} (UnderlyingReal 𝕜 F)17      (inferInstanceAs (NormedAddCommGroup F)) (NormedSpace.restrictScalars ℝ 𝕜 F) := by18  let := NormedSpace.restrictScalars ℝ 𝕜 E19  let := NormedSpace.restrictScalars ℝ 𝕜 F20  let := IsScalarTower.restrictScalars ℝ 𝕜 E21  let := IsScalarTower.restrictScalars ℝ 𝕜 F22  change @HasRadonNikodymProperty.{u, w} E _ (NormedSpace.restrictScalars ℝ 𝕜 E) ↔23    @HasRadonNikodymProperty.{v, w} F _ (NormedSpace.restrictScalars ℝ 𝕜 F)24  let eR : E ≃L[ℝ] F := ContinuousLinearEquiv.equivOfInverse25    (e.toContinuousLinearMap.restrictScalars ℝ)26    (e.symm.toContinuousLinearMap.restrictScalars ℝ)27    e.symm_apply_apply e.apply_symm_apply28  exact RNPBridge.hasRadonNikodymProperty_iff_equiv eR2930end PL1.RNPTransport31