The initial protected stage

This file upgrades the elementary bent-map calculation to an actual map between real Banach spaces carrying the invariant used by the transfinite construction.

noncomputable def ScottishBook155.bentMapL1 (t : ℝ) : OneSum ℝ

The bent seed as a map into the genuine l-one Banach sum.

Equations

• ScottishBook155.bentMapL1 t = WithLp.toLp 1 (ScottishBook155.bentMap t)

theorem ScottishBook155.bentMapL1_injective : Function.Injective bentMapL1

theorem ScottishBook155.bentMapL1_dist_eq (s t : ℝ) : dist (bentMapL1 s) (bentMapL1 t) = l1Dist (bentMap s) (bentMap t)

theorem ScottishBook155.bentMapL1_preservesUpTo : PreservesUpTo (1 / 2) bentMapL1

theorem ScottishBook155.bentMapL1_contraction : dist (bentMapL1 (-1)) (bentMapL1 2) = 1 ∧ dist (-1) 2 = 3

noncomputable def ScottishBook155.bentSeedStage : ProtectedStage (1 / 2)

Stage zero of the claim-14 recursion.

Equations

• One or more equations did not get rendered due to their size.