import Mathlib.MeasureTheory.Function.LpSpace

import Mathlib.MeasureTheory.Function.LpSpace

import Mathlib.Data.Set.Image

import Mathlib.MeasureTheory.Measure.OpenPos

import Mathlib.MeasureTheory.Measure.Typeclasses

import Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace

import Mathlib.Topology.ContinuousMap.Compact

open scoped NNReal ENNReal Topology MeasureTheory Uniformity symmDiff

open scoped BoundedContinuousFunction

open BoundedContinuousFunction

variable [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E]

variable (E p μ)

def MeasureTheory.Lp.boundedContinuousFunction : AddSubgroup (Lp E p μ) :=

AddSubgroup.addSubgroupOf

((ContinuousMap.toAEEqFunAddHom μ).comp (toContinuousMapAddHom α E)).range (Lp E p μ)

variable {E p μ}

theorem MeasureTheory.Lp.mem_boundedContinuousFunction_iff {f : Lp E p μ} :

f ∈ MeasureTheory.Lp.boundedContinuousFunction E p μ ↔

∃ f₀ : α →ᵇ E, f₀.toContinuousMap.toAEEqFun μ = (f : α →ₘ[μ] E) :=

AddSubgroup.mem_addSubgroupOf

namespace BoundedContinuousFunction

variable [IsFiniteMeasure μ]

theorem mem_Lp (f : α →ᵇ E) : f.toContinuousMap.toAEEqFun μ ∈ Lp E p μ := by

refine Lp.mem_Lp_of_ae_bound ‖f‖ ?_

filter_upwards [f.toContinuousMap.coeFn_toAEEqFun μ] with x _

convert f.norm_coe_le_norm x using 2

theorem Lp_nnnorm_le (f : α →ᵇ E) :

‖(⟨f.toContinuousMap.toAEEqFun μ, mem_Lp f⟩ : Lp E p μ)‖₊ ≤

measureUnivNNReal μ ^ p.toReal⁻¹ * ‖f‖₊ := by

apply Lp.nnnorm_le_of_ae_bound

refine (f.toContinuousMap.coeFn_toAEEqFun μ).mono ?_

intro x hx

rw [← NNReal.coe_le_coe, coe_nnnorm, coe_nnnorm]

convert f.norm_coe_le_norm x using 2

theorem Lp_norm_le (f : α →ᵇ E) :

‖(⟨f.toContinuousMap.toAEEqFun μ, mem_Lp f⟩ : Lp E p μ)‖ ≤

measureUnivNNReal μ ^ p.toReal⁻¹ * ‖f‖ :=

Lp_nnnorm_le f

variable (p μ)

def toLpHom [Fact (1 ≤ p)] : NormedAddGroupHom (α →ᵇ E) (Lp E p μ) :=

{ AddMonoidHom.codRestrict ((ContinuousMap.toAEEqFunAddHom μ).comp (toContinuousMapAddHom α E))

(Lp E p μ) mem_Lp with

bound' := ⟨_, Lp_norm_le⟩ }

theorem range_toLpHom [Fact (1 ≤ p)] :

((toLpHom p μ).range : AddSubgroup (Lp E p μ)) =

MeasureTheory.Lp.boundedContinuousFunction E p μ := by

symm

exact AddMonoidHom.addSubgroupOf_range_eq_of_le

((ContinuousMap.toAEEqFunAddHom μ).comp (toContinuousMapAddHom α E))

(by rintro - ⟨f, rfl⟩; exact mem_Lp f : _ ≤ Lp E p μ)

variable (𝕜 : Type*) [Fact (1 ≤ p)]

def toLp [NormedField 𝕜] [NormedSpace 𝕜 E] : (α →ᵇ E) →L[𝕜] Lp E p μ :=

LinearMap.mkContinuous

(LinearMap.codRestrict (Lp.LpSubmodule 𝕜 E p μ)

((ContinuousMap.toAEEqFunLinearMap μ).comp (toContinuousMapLinearMap α E 𝕜)) mem_Lp)

_ Lp_norm_le

theorem coeFn_toLp [NormedField 𝕜] [NormedSpace 𝕜 E] (f : α →ᵇ E) :

toLp (E := E) p μ 𝕜 f =ᵐ[μ] f :=

AEEqFun.coeFn_mk f _

variable {𝕜}

theorem range_toLp [NormedField 𝕜] [NormedSpace 𝕜 E] :

(LinearMap.range (toLp p μ 𝕜 : (α →ᵇ E) →L[𝕜] Lp E p μ)).toAddSubgroup =

MeasureTheory.Lp.boundedContinuousFunction E p μ :=

range_toLpHom p μ

variable {p}

theorem toLp_norm_le [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] :

‖(toLp p μ 𝕜 : (α →ᵇ E) →L[𝕜] Lp E p μ)‖ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ :=

LinearMap.mkContinuous_norm_le _ (measureUnivNNReal μ ^ p.toReal⁻¹).coe_nonneg _

theorem toLp_inj {f g : α →ᵇ E} [μ.IsOpenPosMeasure] [NormedField 𝕜] [NormedSpace 𝕜 E] :

toLp (E := E) p μ 𝕜 f = toLp (E := E) p μ 𝕜 g ↔ f = g := by

refine ⟨fun h => ?_, by tauto⟩

rw [← DFunLike.coe_fn_eq, ← (map_continuous f).ae_eq_iff_eq μ (map_continuous g)]

refine (coeFn_toLp p μ 𝕜 f).symm.trans (EventuallyEq.trans ?_ <| coeFn_toLp p μ 𝕜 g)

rw [h]

theorem toLp_injective [μ.IsOpenPosMeasure] [NormedField 𝕜] [NormedSpace 𝕜 E] :

Function.Injective (⇑(toLp p μ 𝕜 : (α →ᵇ E) →L[𝕜] Lp E p μ)) :=

fun _f _g hfg => (toLp_inj μ).mp hfg

end BoundedContinuousFunction

namespace ContinuousMap

variable [CompactSpace α] [IsFiniteMeasure μ]

variable (𝕜 : Type*) (p μ) [Fact (1 ≤ p)]

def toLp [NormedField 𝕜] [NormedSpace 𝕜 E] : C(α, E) →L[𝕜] Lp E p μ :=

(BoundedContinuousFunction.toLp p μ 𝕜).comp

(linearIsometryBoundedOfCompact α E 𝕜).toLinearIsometry.toContinuousLinearMap

variable {𝕜}

theorem range_toLp [NormedField 𝕜] [NormedSpace 𝕜 E] :

(LinearMap.range (toLp p μ 𝕜 : C(α, E) →L[𝕜] Lp E p μ)).toAddSubgroup =

MeasureTheory.Lp.boundedContinuousFunction E p μ := by

refine SetLike.ext' ?_

have := (linearIsometryBoundedOfCompact α E 𝕜).surjective

convert Function.Surjective.range_comp this (BoundedContinuousFunction.toLp (E := E) p μ 𝕜)

rw [← BoundedContinuousFunction.range_toLp p μ (𝕜 := 𝕜), Submodule.coe_toAddSubgroup,

LinearMap.range_coe]

variable {p}

theorem coeFn_toLp [NormedField 𝕜] [NormedSpace 𝕜 E] (f : C(α, E)) :

toLp (E := E) p μ 𝕜 f =ᵐ[μ] f :=

AEEqFun.coeFn_mk f _

theorem toLp_def [NormedField 𝕜] [NormedSpace 𝕜 E] (f : C(α, E)) :

toLp (E := E) p μ 𝕜 f =

BoundedContinuousFunction.toLp (E := E) p μ 𝕜 (linearIsometryBoundedOfCompact α E 𝕜 f) :=

rfl

theorem toLp_comp_toContinuousMap [NormedField 𝕜] [NormedSpace 𝕜 E] (f : α →ᵇ E) :

toLp (E := E) p μ 𝕜 f.toContinuousMap = BoundedContinuousFunction.toLp (E := E) p μ 𝕜 f :=

rfl

theorem coe_toLp [NormedField 𝕜] [NormedSpace 𝕜 E] (f : C(α, E)) :

(toLp (E := E) p μ 𝕜 f : α →ₘ[μ] E) = f.toAEEqFun μ :=

rfl

theorem toLp_injective [μ.IsOpenPosMeasure] [NormedField 𝕜] [NormedSpace 𝕜 E] :

Function.Injective (⇑(toLp p μ 𝕜 : C(α, E) →L[𝕜] Lp E p μ)) :=

(BoundedContinuousFunction.toLp_injective _).comp (linearIsometryBoundedOfCompact α E 𝕜).injective

theorem toLp_inj {f g : C(α, E)} [μ.IsOpenPosMeasure] [NormedField 𝕜] [NormedSpace 𝕜 E] :

toLp (E := E) p μ 𝕜 f = toLp (E := E) p μ 𝕜 g ↔ f = g :=

(toLp_injective μ).eq_iff

variable {μ}

theorem hasSum_of_hasSum_Lp {β : Type*} [μ.IsOpenPosMeasure] [NormedField 𝕜] [NormedSpace 𝕜 E]

{g : β → C(α, E)} {f : C(α, E)} (hg : Summable g)

(hg2 : HasSum (toLp (E := E) p μ 𝕜 ∘ g) (toLp (E := E) p μ 𝕜 f)) : HasSum g f := by

convert Summable.hasSum hg

exact toLp_injective μ (hg2.unique ((toLp p μ 𝕜).hasSum <| Summable.hasSum hg))

variable (μ) [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E]

theorem toLp_norm_eq_toLp_norm_coe :

‖(toLp p μ 𝕜 : C(α, E) →L[𝕜] Lp E p μ)‖ =

‖(BoundedContinuousFunction.toLp p μ 𝕜 : (α →ᵇ E) →L[𝕜] Lp E p μ)‖ :=

ContinuousLinearMap.opNorm_comp_linearIsometryEquiv _ _

theorem toLp_norm_le :

‖(toLp p μ 𝕜 : C(α, E) →L[𝕜] Lp E p μ)‖ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ := by

rw [toLp_norm_eq_toLp_norm_coe]

exact BoundedContinuousFunction.toLp_norm_le μ

end ContinuousMap

set_option linter.style.longFile 1800