ComplementedSubspace/Ambient.lean

1import Mathlib.Analysis.Normed.Lp.PiLp

2import Mathlib.Analysis.Normed.Lp.lpSpace

3import Mathlib.Analysis.Normed.Operator.NormedSpace

4import Mathlib.Data.PNat.Defs

5import Mathlib.Tactic.NormNum

7/-!

8# The ambient countable sum

10The finite blocks use the counting-measure `ℓᵖ` norm. The outer space is the

11dependent `ℓ²` sum of these blocks. This file constructs the actual normed and

12complete spaces and their coordinate projections; it does not claim the

13Banach lattice or uniform convexity instances have been proved.

14-/

16noncomputable section

18open scoped ENNReal Topology

20namespace ComplementedSubspace

22/-- The parameters required by the real main theorem. -/

23structure BlockParameters where

24 dimension : ℕ → ℕ+

25 exponent : ℕ → ℝ

26 two_lt_exponent : ∀ j, 2 < exponent j

27 exponent_le_three : ∀ j, exponent j ≤ 3

28 exponent_antitone : Antitone exponent

29 exponent_tendsto : Filter.Tendsto exponent Filter.atTop (𝓝 2)

31instance (a : BlockParameters) (j : ℕ) :

32 Fact (1 ≤ ENNReal.ofReal (a.exponent j)) := by

33 constructor

34 have h : (1 : ℝ) ≤ a.exponent j :=

35 (by norm_num : (1 : ℝ) ≤ 2).trans (a.two_lt_exponent j).le

36 simpa using ENNReal.ofReal_le_ofReal h

38/-- A finite real block with its genuine `ℓᵖ` norm. -/

39abbrev Block (a : BlockParameters) (j : ℕ) :=

40 PiLp (ENNReal.ofReal (a.exponent j)) (fun _ : Fin (a.dimension j) => ℝ)

42/-- The actual ambient space `(⨁ j, ℓ^(p j)^(N j))₂`. -/

43abbrev Ambient (a : BlockParameters) := lp (Block a) 2

45example (a : BlockParameters) (j : ℕ) : CompleteSpace (Block a j) := inferInstance

46example (a : BlockParameters) : NormedSpace ℝ (Ambient a) := inferInstance

47example (a : BlockParameters) : CompleteSpace (Ambient a) := inferInstance

49/-- Isometric inclusion of one block into the ambient space. -/

50def blockInclusion (a : BlockParameters) (j : ℕ) : Block a j →L[ℝ] Ambient a :=

51 lp.singleContinuousLinearMap ℝ (Block a) 2 j

53/-- Evaluation at one block. -/

54def blockEvaluation (a : BlockParameters) (j : ℕ) : Ambient a →L[ℝ] Block a j :=

55 lp.evalCLM ℝ (Block a) 2 j

57/-- Projection onto the chosen block, as an endomorphism of the ambient space. -/

58def blockProjection (a : BlockParameters) (j : ℕ) : Ambient a →L[ℝ] Ambient a :=

59 (blockInclusion a j).comp (blockEvaluation a j)

61@[simp]

62theorem blockEvaluation_blockInclusion (a : BlockParameters) (j : ℕ) (x : Block a j) :

63 blockEvaluation a j (blockInclusion a j x) = x := by

64 change (lp.single 2 j x) j = x

65 simp

67@[simp]

68theorem norm_blockInclusion (a : BlockParameters) (j : ℕ) (x : Block a j) :

69 ‖blockInclusion a j x‖ = ‖x‖ := by

70 exact lp.norm_single (by norm_num : (0 : ℝ≥0∞) < 2) j x

72theorem blockProjection_idempotent (a : BlockParameters) (j : ℕ) :

73 (blockProjection a j).comp (blockProjection a j) = blockProjection a j := by

74 ext x

75 simp [blockProjection]

77theorem norm_blockProjection_apply_le (a : BlockParameters) (j : ℕ) (x : Ambient a) :

78 ‖blockProjection a j x‖ ≤ ‖x‖ := by

79 change ‖blockInclusion a j (blockEvaluation a j x)‖ ≤ ‖x‖

80 rw [norm_blockInclusion]

81 exact lp.norm_apply_le_norm (by norm_num : (2 : ℝ≥0∞) ≠ 0) x j

83theorem norm_blockProjection_le_one (a : BlockParameters) (j : ℕ) :

84 ‖blockProjection a j‖ ≤ 1 := by

85 apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one

86 intro x

87 simpa using norm_blockProjection_apply_le a j x

89/-- Every vector is the unconditionally convergent sum of its block components. -/

90theorem hasSum_blockProjection (a : BlockParameters) (x : Ambient a) :

91 HasSum (fun j => blockProjection a j x) x := by

92 exact lp.hasSum_single (by norm_num : (2 : ℝ≥0∞) ≠ ⊤) x

94end ComplementedSubspace