Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

Actual PBPS projected reflection rotation and exact pair energy

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualProjectedRotation.actual_projected_rotation · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including the explicit rank-zero extension. Let V:E→ℝ be C², 0<α≤β, and assume α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v. Assume η>0 and βη≤1. Define μ(dx) proportional to exp(−V(x))dx, J as the law of (X,X+√η Z) for independent X~μ and Z~N(0,I), ν=J.snd, and Λ as the law of (Y,2X−Y) under J. These are probability laws. Put mY=comap(snd), H_P=L² classes measurable with respect to mY, P=i∘E[·|Y] and the canonical M:u↦u∘snd. Then H_P=ran(P), P is identity on H_P, and there exists an onto linear isometry e:L²(ν;ℝ)≃H_P with i e=M. There is a Markov kernel S whose every-state normalized law is S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)); Λ.IsCondKernel S and both Λ marginals equal ν. The same joint reflection F(x,y)=(x,2x−y) gives the involutive selfadjoint isometry U, with Uf=f∘F J-almost everywhere for every f. There is a bounded selfadjoint T on the full real L²(ν), with ‖Tu‖≤‖u‖, Tu(y)=∫u(x)S(y,dx) ν-almost everywhere for each u, and preserved integral. On H_P put A=PUP restricted via i and orthogonal projection, and B=(I_J−P)UPi:H_P→L²(J). Then A=eTe⁻¹ is selfadjoint and contractive, PB=0. There is a bounded positive operator Γ on the real scalar-valued L² space with Γ²=I−T². For the SAME transported Γ_P=eΓe⁻¹, positivity holds and Γ_P²=I_H_P−A²=B*B. There is q∈L²(ν;ℝ) equal to one ν-almost everywhere, with Tq=q and ⟨q,u⟩=∫u dν for every u. Set q_P=e q and H_P^0=ker⟨q_P,·⟩, with its inherited Hilbert structure. Membership is exactly zero ν-mean after e⁻¹. The SAME Γ_P annihilates q_P. Put γ=2√(αη)/(1+αη)>0. There exists Γ_0:H_P^0→H_P^0 equal under inclusion to the restriction of Γ_P, positive with Γ_0−γ I positive. Γ_0 is a unit in the algebra of bounded real operators. There exists a bounded real Inv on this SAME centered space with Inv Γ_0=Γ_0 Inv=I and ‖Inv‖≤1/γ. All probability, normalization, range, root, centering, spectral-gap, unit and inverse facts are internally derived from the original inputs; none is an additional public premise. αη=1 and rank-zero E remain legal. No inverse on full H_P is asserted. Define the actual closed conditional-mean-zero space H_perp=ker P in L²(J;ℝ), with its inherited complete Hilbert structure; this is not merely the globally zero-mean joint space. There exists B_0:H_P^0→H_perp whose inclusion equals B i_0. There exists V_0:H_P^0→H_perp with V_0=B_0 Inv, B_0=V_0 Γ_0, V_0* V_0=I and ‖V_0 f‖=‖f‖ for every f∈H_P^0. All these objects and identities are conclusions from the same original inputs. There exists the canonical bounded residual map R:L²(J;ℝ)→H_perp with i_perp Rg=g−Pg for every joint g. The SAME ambient adjoint satisfies B* g=i_0 B_0* Rg for every joint g; the printed intrinsic block adjoint is recovered on H_perp. For every actual joint f∈L²(J;ℝ) with ∫f dJ=0, there exists f_P∈H_P^0 whose inclusion is E[f|Y]. Put f_perp=Rf and f_V=V_0* f_perp∈the SAME H_P^0. Then B* i_perp f_perp=i_0 Γ_0 f_V=Γ_P i_0 f_V, ‖f‖²=‖f_P‖²+‖f_perp‖² and ‖f_V‖≤‖f_perp‖. The global zero-mean condition is a quantified input restriction to this concluded implication, not an extra assumption on the potential or an operator certificate. The SAME root commutes with T and its transport commutes with A. The SAME Inv on H_P^0 is selfadjoint. There exists an internally constructed A_0:H_P^0→H_P^0 whose inclusion equals A after inclusion; it is selfadjoint,commutes with Γ_0,satisfies A_0²+Γ_0²=I,and commutes with the SAME Inv. For the same U,R and inclusion of H_perp=ker P, define D=R U inclusion. Its full-domain identity V0*D=-A0 V0* is retained. For EVERY globally mean-zero f in L2(J), let fP be its actual centered conditional-expectation component, fperp=R f and fV=V0* fperp. Define the actual output g=U(P f-(f-P f)), not an abstract pair chosen to satisfy a matrix identity. The theorem proves its global mean is zero internally from invariance of the actual reflected augmentation law and preservation of the integral by conditional expectation. Let gP be the actual centered conditional-expectation component of this SAME g, gperp=R g and gV=V0* gperp. Then gP=A0 fP-Gamma0 fV, gV=Gamma0 fP+A0 fV, and ||gP||^2+||gV||^2=||fP||^2+||fV||^2. Both output components are produced by these actual conditional/polar semantics before proving the formulas; neither is defined as its right-hand side. All previous law/kernel/root/inverse/polar/full-micro and centered-observable conclusions persist with the SAME twelve witnesses and the original six analytic caller conditions. No surjectivity, sharp-energy68 bound, extra regularity or zero-output-mean premise is introduced. One private literal Prop stores the complete sealed mathematical conclusion; it supplies no proof provider or additional hypothesis. The actual B21 corrector change, B4 dynamics, weak H1/B2, main convergence, invariance/nonexplosion, implementation errors/caps, expected-query costs and actual-input composition remain separate obligations.

\[g=U(Pf-(f-Pf)),\quad g_P=A_0f_P-\Gamma_0f_V,\quad g_V=\Gamma_0f_P+A_0f_V,\quad \|g_P\|^2+\|g_V\|^2=\|f_P\|^2+\|f_V\|^2.\]
Lean statement · actual_projected_rotation

Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including the explicit rank-zero extension. Let V:E→ℝ be C², 0<α≤β, and assume α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v. Assume η>0 and βη≤1. Define μ(dx) proportional to exp(−V(x))dx, J as the law of (X,X+√η Z) for independent X~μ and Z~N(0,I), ν=J.snd, and Λ as the law of (Y,2X−Y) under J. These are probability laws. Put mY=comap(snd), H_P=L² classes measurable with respect to mY, P=i∘E[·|Y] and the canonical M:u↦u∘snd. Then H_P=ran(P), P is identity on H_P, and there exists an onto linear isometry e:L²(ν;ℝ)≃H_P with i e=M. There is a Markov kernel S whose every-state normalized law is S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)); Λ.IsCondKernel S and both Λ marginals equal ν. The same joint reflection F(x,y)=(x,2x−y) gives the involutive selfadjoint isometry U, with Uf=f∘F J-almost everywhere for every f. There is a bounded selfadjoint T on the full real L²(ν), with ‖Tu‖≤‖u‖, Tu(y)=∫u(x)S(y,dx) ν-almost everywhere for each u, and preserved integral. On H_P put A=PUP restricted via i and orthogonal projection, and B=(I_J−P)UPi:H_P→L²(J). Then A=eTe⁻¹ is selfadjoint and contractive, PB=0. There is a bounded positive operator Γ on the real scalar-valued L² space with Γ²=I−T². For the SAME transported Γ_P=eΓe⁻¹, positivity holds and Γ_P²=I_H_P−A²=B*B. There is q∈L²(ν;ℝ) equal to one ν-almost everywhere, with Tq=q and ⟨q,u⟩=∫u dν for every u. Set q_P=e q and H_P^0=ker⟨q_P,·⟩, with its inherited Hilbert structure. Membership is exactly zero ν-mean after e⁻¹. The SAME Γ_P annihilates q_P. Put γ=2√(αη)/(1+αη)>0. There exists Γ_0:H_P^0→H_P^0 equal under inclusion to the restriction of Γ_P, positive with Γ_0−γ I positive. Γ_0 is a unit in the algebra of bounded real operators. There exists a bounded real Inv on this SAME centered space with Inv Γ_0=Γ_0 Inv=I and ‖Inv‖≤1/γ. All probability, normalization, range, root, centering, spectral-gap, unit and inverse facts are internally derived from the original inputs; none is an additional public premise. αη=1 and rank-zero E remain legal. No inverse on full H_P is asserted. Define the actual closed conditional-mean-zero space H_perp=ker P in L²(J;ℝ), with its inherited complete Hilbert structure; this is not merely the globally zero-mean joint space. There exists B_0:H_P^0→H_perp whose inclusion equals B i_0. There exists V_0:H_P^0→H_perp with V_0=B_0 Inv, B_0=V_0 Γ_0, V_0* V_0=I and ‖V_0 f‖=‖f‖ for every f∈H_P^0. All these objects and identities are conclusions from the same original inputs. There exists the canonical bounded residual map R:L²(J;ℝ)→H_perp with i_perp Rg=g−Pg for every joint g. The SAME ambient adjoint satisfies B* g=i_0 B_0* Rg for every joint g; the printed intrinsic block adjoint is recovered on H_perp. For every actual joint f∈L²(J;ℝ) with ∫f dJ=0, there exists f_P∈H_P^0 whose inclusion is E[f|Y]. Put f_perp=Rf and f_V=V_0* f_perp∈the SAME H_P^0. Then B* i_perp f_perp=i_0 Γ_0 f_V=Γ_P i_0 f_V, ‖f‖²=‖f_P‖²+‖f_perp‖² and ‖f_V‖≤‖f_perp‖. The global zero-mean condition is a quantified input restriction to this concluded implication, not an extra assumption on the potential or an operator certificate. The SAME root commutes with T and its transport commutes with A. The SAME Inv on H_P^0 is selfadjoint. There exists an internally constructed A_0:H_P^0→H_P^0 whose inclusion equals A after inclusion; it is selfadjoint,commutes with Γ_0,satisfies A_0²+Γ_0²=I,and commutes with the SAME Inv. For the same U,R and inclusion of H_perp=ker P, define D=R U inclusion. Its full-domain identity V0*D=-A0 V0* is retained. For EVERY globally mean-zero f in L2(J), let fP be its actual centered conditional-expectation component, fperp=R f and fV=V0* fperp. Define the actual output g=U(P f-(f-P f)), not an abstract pair chosen to satisfy a matrix identity. The theorem proves its global mean is zero internally from invariance of the actual reflected augmentation law and preservation of the integral by conditional expectation. Let gP be the actual centered conditional-expectation component of this SAME g, gperp=R g and gV=V0* gperp. Then gP=A0 fP-Gamma0 fV, gV=Gamma0 fP+A0 fV, and ||gP||^2+||gV||^2=||fP||^2+||fV||^2. Both output components are produced by these actual conditional/polar semantics before proving the formulas; neither is defined as its right-hand side. All previous law/kernel/root/inverse/polar/full-micro and centered-observable conclusions persist with the SAME twelve witnesses and the original six analytic caller conditions. No surjectivity, sharp-energy68 bound, extra regularity or zero-output-mean premise is introduced. One private literal Prop stores the complete sealed mathematical conclusion; it supplies no proof provider or additional hypothesis. The actual B21 corrector change, B4 dynamics, weak H1/B2, main convergence, invariance/nonexplosion, implementation errors/caps, expected-query costs and actual-input composition remain separate obligations.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
theorem actual_projected_rotation
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ)*‖v‖^2)
    (hη : 0 < η) (hβη : (β : ℝ)*η ≤ 1) : actual_projected_rotation_statement (E:=E) (V:=V) (α:=α) (β:=β) (η:=η) hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_projected_rotation_statement

This literal definition stores the complete proposition asserted above. It supplies no mathematical proof or additional hypothesis; the theorem proof must establish its value.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
private def actual_projected_rotation_statement
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ)*‖v‖^2)
    (hη : 0 < η) (hβη : (β : ℝ)*η ≤ 1) : Prop :=
    let μ := (volume : Measure E).tilted (fun x => -V x)
    let J := (μ.prod (stdGaussian E)).map
      (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
    let ν := J.snd
    let Λ := J.map (fun p : E × E => (p.2,(2 : ℝ) • p.1-p.2))
    let F := fun p : E × E => (p.1,(2 : ℝ) • p.1-p.2)
    let mY := MeasurableSpace.comap Prod.snd (inferInstance : MeasurableSpace E)
    letI : MeasurableSpace (E × E) := Prod.instMeasurableSpace
    letI : Fact (mY ≤ (inferInstance : MeasurableSpace (E × E))) :=
      ⟨measurable_snd.comap_le⟩
    let HP := lpMeas ℝ ℝ mY 2 J
    let P : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J :=
      HP.subtypeL ∘L condExpL2 ℝ ℝ (μ := J) measurable_snd.comap_le
    let hp : MeasurePreserving (Prod.snd : E × E → E) J ν := ⟨measurable_snd,rfl⟩
    let M : Lp ℝ 2 ν →ₗᵢ[ℝ] Lp ℝ 2 J := Lp.compMeasurePreservingₗᵢ ℝ Prod.snd hp
    IsProbabilityMeasure μ ∧ IsProbabilityMeasure J ∧ IsProbabilityMeasure ν ∧
    HP = P.toLinearMap.range ∧
    (∀ f : HP, P (f : Lp ℝ 2 J) = f) ∧
    ∃ S : Kernel E E, IsMarkovKernel S ∧
      (∀ y, S y = (volume : Measure E).tilted
        (fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η))) ∧
      Λ.IsCondKernel S ∧ Λ.fst = ν ∧ Λ.snd = ν ∧
      ∃ e : Lp ℝ 2 ν ≃ₗᵢ[ℝ] HP,
        (∀ u : Lp ℝ 2 ν, (e u : Lp ℝ 2 J) = M u) ∧
        ∃ U : Lp ℝ 2 J →ₗᵢ[ℝ] Lp ℝ 2 J,
          (∀ g : Lp ℝ 2 J, (U g : E × E → ℝ) =ᵐ[J] g ∘ F) ∧
          Function.Involutive U ∧ IsSelfAdjoint U.toContinuousLinearMap ∧
          ∃ T : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
            IsSelfAdjoint T ∧
            (∀ u : Lp ℝ 2 ν,
              ‖T u‖ ≤ ‖u‖ ∧
              (T u : E → ℝ) =ᵐ[ν] (fun y => ∫ x, u x ∂S y) ∧
              (∫ y, T u y ∂ν) = ∫ y, u y ∂ν) ∧
            let A : HP →L[ℝ] HP :=
              HP.orthogonalProjectionOnto ∘L U.toContinuousLinearMap ∘L HP.subtypeL
            let B : HP →L[ℝ] Lp ℝ 2 J :=
              (((1 : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J)-P)*U.toContinuousLinearMap*P) ∘L HP.subtypeL
            A = e.conjStarAlgEquiv T ∧ IsSelfAdjoint A ∧
            (∀ f : HP, ‖A f‖ ≤ ‖f‖) ∧
            (∀ f : HP, P (B f) = 0) ∧
            ∃ Γ : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
              Γ.IsPositive ∧ Γ*Γ=(1 : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν)-T*T ∧
              Commute Γ T ∧
              let ΓP : HP →L[ℝ] HP := e.conjStarAlgEquiv Γ
              ΓP.IsPositive ∧ ΓP*ΓP=(1 : HP →L[ℝ] HP)-A*A ∧
              Commute ΓP A ∧
              B.adjoint ∘L B = ΓP*ΓP ∧
              ∃ q : Lp ℝ 2 ν,
                (q : E → ℝ) =ᵐ[ν] (fun _ => (1 : ℝ)) ∧ T q = q ∧
                (∀ u : Lp ℝ 2 ν, inner ℝ q u = ∫ y, u y ∂ν) ∧
                let qP : HP := e q
                let HP0 := (innerSL ℝ qP).ker
                letI : NormedAddCommGroup HP0 := HP0.normedAddCommGroup
                letI : InnerProductSpace ℝ HP0 := HP0.innerProductSpace
                letI : CompleteSpace HP0 := (innerSL ℝ qP).isClosed_ker.completeSpace_coe
                let γ : ℝ := 2*Real.sqrt ((α : ℝ)*η)/(1+(α : ℝ)*η)
                (∀ f : HP, f ∈ HP0 ↔ (∫ y, (e.symm f) y ∂ν) = 0) ∧
                ΓP qP = 0 ∧ 0 < γ ∧
                ∃ ΓP0 : HP0 →L[ℝ] HP0,
                  (∀ f : HP0, (ΓP0 f : HP) = ΓP (f : HP)) ∧
                  ΓP0.IsPositive ∧ (ΓP0-γ • (1 : HP0 →L[ℝ] HP0)).IsPositive ∧
                  IsUnit ΓP0 ∧
                  ∃ Inv : HP0 →L[ℝ] HP0,
                    Inv*ΓP0=(1 : HP0 →L[ℝ] HP0) ∧
                    ΓP0*Inv=(1 : HP0 →L[ℝ] HP0) ∧ ‖Inv‖ ≤ 1/γ ∧
                    IsSelfAdjoint Inv ∧
                    ∃ A0 : HP0 →L[ℝ] HP0,
                      (∀ u : HP0, (A0 u : HP)=A (u : HP)) ∧
                      IsSelfAdjoint A0 ∧ Commute A0 ΓP0 ∧
                      A0*A0+ΓP0*ΓP0=(1 : HP0 →L[ℝ] HP0) ∧
                      Commute A0 Inv ∧
                    let Hperp := P.ker
                    letI : NormedAddCommGroup Hperp := Hperp.normedAddCommGroup
                    letI : InnerProductSpace ℝ Hperp := Hperp.innerProductSpace
                    letI : CompleteSpace Hperp := P.isClosed_ker.completeSpace_coe
                    ∃ B0 : HP0 →L[ℝ] Hperp,
                      (∀ f : HP0, (B0 f : Lp ℝ 2 J) = B (f : HP)) ∧
                      ∃ V0 : HP0 →L[ℝ] Hperp,
                        V0 = B0 ∘L Inv ∧ B0 = V0 ∘L ΓP0 ∧
                        V0.adjoint ∘L V0 = (1 : HP0 →L[ℝ] HP0) ∧
                        (∀ f : HP0, ‖V0 f‖ = ‖f‖) ∧
                        ∃ R : Lp ℝ 2 J →L[ℝ] Hperp,
                          (∀ g : Lp ℝ 2 J, (R g : Lp ℝ 2 J)=g-P g) ∧
                          (∀ g : Lp ℝ 2 J,
                            B.adjoint g=HP0.subtypeL (B0.adjoint (R g))) ∧
                          let D : Hperp →L[ℝ] Hperp :=
                            R ∘L U.toContinuousLinearMap ∘L Hperp.subtypeL
                          (∀ h : Hperp, (D h : Lp ℝ 2 J)=
                            U (h : Lp ℝ 2 J)-P (U (h : Lp ℝ 2 J))) ∧
                          V0.adjoint ∘L D = -(A0 ∘L V0.adjoint) ∧
                          (∀ f : Lp ℝ 2 J, (∫ z, f z ∂J)=0 →
                            ∃ fP : HP0,
                              HP0.subtypeL fP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le f ∧
                              let fperp : Hperp := R f
                              let fV : HP0 := V0.adjoint fperp
                              B.adjoint (fperp : Lp ℝ 2 J)=HP0.subtypeL (ΓP0 fV) ∧
                              HP0.subtypeL (ΓP0 fV)=ΓP (HP0.subtypeL fV) ∧
                              ‖f‖^2=‖fP‖^2+‖fperp‖^2 ∧ ‖fV‖≤‖fperp‖ ∧
                              let g : Lp ℝ 2 J := U (P f-(f-P f))
                              (∫ z, g z ∂J)=0 ∧
                              ∃ gP : HP0,
                                HP0.subtypeL gP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le g ∧
                                let gperp : Hperp := R g
                                let gV : HP0 := V0.adjoint gperp
                                gP=A0 fP-ΓP0 fV ∧
                                gV=ΓP0 fP+A0 fV ∧
                                ‖gP‖^2+‖gV‖^2=‖fP‖^2+‖fV‖^2)

Exact module and namespace context

Proof roadmap

  1. 1Retain the same actual probability geometry and operators

    Unfold the literal proposition and apply the independently accepted original-input parent. Retain its actual law, conditional kernel, reflection, centered defect root, inverse, polar isometry and globally centered-observable decomposition. The complete macro and micro subspaces have their inherited Hilbert structures.

  2. 2Prove mean preservation from the actual law

    The current U acts almost everywhere by the actual reflection F. The independently compiled augmentation invariance gives F#J=J, so change of variables preserves the integral. Conditional expectation preserves the full integral as well. Since J is a probability law, every L2 observable is integrable, and subtraction of actual representatives is legitimate.

  3. 3Identify actual macro and micro compressions

    Include the centered macro space into the joint L2 space by iota. Orthogonality to ker P follows from selfadjointness of P. The same A0 and B0 split the reflected macro vector. The actual residual and polar-adjoint identities then identify its micro component without any range or surjectivity premise.

  4. 4Obtain the scalar energy and cross-term identities

    Positivity makes Gamma0 selfadjoint; A0 is selfadjoint already. Test A0^2+Gamma0^2=I against u to get the scalar norm identity. Move A0 and Gamma0 across the inner products and use their commutation to identify the two mixed terms.

  5. 5Produce the components of the actual reflected input

    Start with an arbitrary globally centered f. Obtain fP from the same actual conditional expectation and fV=V0*Rf. Define g by the actual U action. Integral preservation gives mean(g)=mean(f)-[mean(f)-mean(f)]=0, so the SAME existing producer applies to g and supplies its actual gP. No zero-output-mean premise or RHS-defined component is used.

  6. 6Derive the actual macro rotation by inner-product separation

    For every centered macro test vector u, move P and U across the inner product using selfadjointness. Split U iota u into its actual macro/micro components; the cross-subspace terms vanish by orthogonality. The adjoint relation B0* fperp=Gamma0 fV and selfadjoint A0 identify the remaining terms. Separation identifies the already produced gP.

  7. 7Derive the actual polar rotation on the full micro space

    Linearity of U,R and V0* gives the reflected macro contribution Gamma0 fP minus the reflected micro contribution V0*D fperp. Apply the full-domain intertwining identity to this actual fperp in ker P. This yields the formula for gV=V0*Rg on its actual output semantics.

  8. 8Cancel mixed terms and retain every original witness

    Expand the squared norms of the two formulas. The opposite mixed terms cancel by the cross-term identity, and the two scalar energy identities reduce the remaining sum to the input pair energy. Reassemble the complete original proposition with the same twelve witnesses. This is the projected rotation ingredient consumed by the subsequent actual B21 corrector change, not the remaining dynamics or main sampling theorem.

Full assumptions and notation

All objects and hypotheses

  • Finite-dimensional real Hilbert Borel base E with canonical volume, including the disclosed rank-zero extension; V is C²; 0<α≤β; both global Hessian bounds; η>0 and βη≤1.
  • Canonical normalized laws/kernel, onto pullback e, SAME U/T, full and centered roots, exact centering, gap, unit and bounded inverse are conclusions. Conditional actions are per-observable AE. L² is not assumed finite-dimensional.
  • γ=2√(αη)/(1+αη); the inverse acts only on H_P^0=ker⟨e1,·⟩ with inherited Hilbert structure; the legal endpoint αη=1 is retained.
  • H_perp is exactly ker P (conditional expectation given Y), while H_P^0 is the zero ν-mean macroscopic space. Their complete Hilbert structures, B_0 and V_0 are internally constructed; no onto-kerP or coisometry assumption is introduced.
  • The concluded global-input implication quantifies every f∈L²(J) with integral zero. R,conditional centering,constant annihilation,adjoint range and norm decomposition are derived internally. Private statement definitions expand literally to the original sealed propositions and add no premise.
  • The global output mean, actual projected component formulas and pair-energy identity are internally proved conclusions. There is no additional zero-output-mean, onto-V0, sharp-energy or higher-smoothness hypothesis.

Mathematical proof

1. Retain the same actual probability geometry and operators

Unfold the literal proposition and apply the independently accepted original-input parent. Retain its actual law, conditional kernel, reflection, centered defect root, inverse, polar isometry and globally centered-observable decomposition. The complete macro and micro subspaces have their inherited Hilbert structures.

\[H_P^0=\ker\langle q_P,\cdot\rangle,\quad H_\perp=\ker P,\quad Rf=f-Pf.\]
Corresponding Lean step
  unfold actual_projected_rotation_statement
  classical
  let μ := (volume : Measure E).tilted (fun x => -V x)
  let J := (μ.prod (stdGaussian E)).map
    (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
  let ν := J.snd
  let mY : MeasurableSpace (E × E) := MeasurableSpace.comap Prod.snd (inferInstance : MeasurableSpace E)
  letI : MeasurableSpace (E × E) := Prod.instMeasurableSpace
  letI : Fact (mY ≤ (inferInstance : MeasurableSpace (E × E))) := ⟨measurable_snd.comap_le⟩
  let HP := lpMeas ℝ ℝ mY 2 J
  letI : NormedAddCommGroup HP := HP.normedAddCommGroup
  letI : InnerProductSpace ℝ HP := HP.innerProductSpace
  let P : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J :=
    HP.subtypeL ∘L condExpL2 ℝ ℝ (μ := J) measurable_snd.comap_le
  have hBase := AutoSamplingTheory.ExampleCases.ProximalBPS.ReflectionIntertwining.actual_reflection_intertwining
    (E:=E) (V:=V) (α:=α) (β:=β) (η:=η) hα hαβ hV hH hη hβη
  have parentSlice0 := hBase
  have hμ := parentSlice0.1
  have parentSlice1 := parentSlice0.2
  have hJ := parentSlice1.1
  have parentSlice2 := parentSlice1.2
  have hν := parentSlice2.1
  have parentSlice3 := parentSlice2.2
  have hRange := parentSlice3.1
  have parentSlice4 := parentSlice3.2
  have hPf := parentSlice4.1
  have parentSlice5 := parentSlice4.2
  obtain ⟨S, parentSlice6⟩ := parentSlice5
  have hS := parentSlice6.1
  have parentSlice7 := parentSlice6.2
  have hSd := parentSlice7.1
  have parentSlice8 := parentSlice7.2
  have hSc := parentSlice8.1
  have parentSlice9 := parentSlice8.2
  have hSf := parentSlice9.1
  have parentSlice10 := parentSlice9.2
  have hSs := parentSlice10.1
  have parentSlice11 := parentSlice10.2
  obtain ⟨e, parentSlice12⟩ := parentSlice11
  have he := parentSlice12.1
  have parentSlice13 := parentSlice12.2
  obtain ⟨U, parentSlice14⟩ := parentSlice13
  have hU := parentSlice14.1
  have parentSlice15 := parentSlice14.2
  have hUi := parentSlice15.1
  have parentSlice16 := parentSlice15.2
  have hUs := parentSlice16.1
  have parentSlice17 := parentSlice16.2
  obtain ⟨T, parentSlice18⟩ := parentSlice17
  have hTs := parentSlice18.1
  have parentSlice19 := parentSlice18.2
  have hAll := parentSlice19.1
  have parentSlice20 := parentSlice19.2
  have hAeq := parentSlice20.1
  have parentSlice21 := parentSlice20.2
  have hAs := parentSlice21.1
  have parentSlice22 := parentSlice21.2
  have hAn := parentSlice22.1
  have parentSlice23 := parentSlice22.2
  have hPB := parentSlice23.1
  have parentSlice24 := parentSlice23.2
  obtain ⟨Γ, parentSlice25⟩ := parentSlice24
  have hΓ := parentSlice25.1
  have parentSlice26 := parentSlice25.2
  have hΓSq := parentSlice26.1
  have parentSlice27 := parentSlice26.2
  have hCommRoot := parentSlice27.1
  have parentSlice28 := parentSlice27.2
  have hΓP := parentSlice28.1
  have parentSlice29 := parentSlice28.2
  have hΓPSq := parentSlice29.1
  have parentSlice30 := parentSlice29.2
  have hCommP := parentSlice30.1
  have parentSlice31 := parentSlice30.2
  have hGram := parentSlice31.1
  have parentSlice32 := parentSlice31.2
  obtain ⟨q, parentSlice33⟩ := parentSlice32
  have hqa := parentSlice33.1
  have parentSlice34 := parentSlice33.2
  have hTq := parentSlice34.1
  have parentSlice35 := parentSlice34.2
  have hq := parentSlice35.1
  have parentSlice36 := parentSlice35.2
  have hCenter := parentSlice36.1
  have parentSlice37 := parentSlice36.2
  have hΓPq := parentSlice37.1
  have parentSlice38 := parentSlice37.2
  have hγ := parentSlice38.1
  have parentSlice39 := parentSlice38.2
  obtain ⟨ΓP0, parentSlice40⟩ := parentSlice39
  have hΓP0 := parentSlice40.1
  have parentSlice41 := parentSlice40.2
  have hPos0 := parentSlice41.1
  have parentSlice42 := parentSlice41.2
  have hOrder0 := parentSlice42.1
  have parentSlice43 := parentSlice42.2
  have hUnit := parentSlice43.1
  have parentSlice44 := parentSlice43.2
  obtain ⟨Inv, parentSlice45⟩ := parentSlice44
  have hLeft := parentSlice45.1
  have parentSlice46 := parentSlice45.2
  have hRight := parentSlice46.1
  have parentSlice47 := parentSlice46.2
  have hNormInv := parentSlice47.1
  have parentSlice48 := parentSlice47.2
  have hInvSelf := parentSlice48.1
  have parentSlice49 := parentSlice48.2
  obtain ⟨A0, parentSlice50⟩ := parentSlice49
  have hA0 := parentSlice50.1
  have parentSlice51 := parentSlice50.2
  have hA0self := parentSlice51.1
  have parentSlice52 := parentSlice51.2
  have hComm0 := parentSlice52.1
  have parentSlice53 := parentSlice52.2
  have hSquare0 := parentSlice53.1
  have parentSlice54 := parentSlice53.2
  have hCommInv := parentSlice54.1
  have parentSlice55 := parentSlice54.2
  obtain ⟨B0, parentSlice56⟩ := parentSlice55
  have hB0 := parentSlice56.1
  have parentSlice57 := parentSlice56.2
  obtain ⟨V0, parentSlice58⟩ := parentSlice57
  have hVdef := parentSlice58.1
  have parentSlice59 := parentSlice58.2
  have hFactor := parentSlice59.1
  have parentSlice60 := parentSlice59.2
  have hVadj := parentSlice60.1
  have parentSlice61 := parentSlice60.2
  have hVnorm := parentSlice61.1
  have parentSlice62 := parentSlice61.2
  obtain ⟨R, parentSlice63⟩ := parentSlice62
  have hR := parentSlice63.1
  have parentSlice64 := parentSlice63.2
  have hAmbient := parentSlice64.1
  have parentSlice65 := parentSlice64.2
  have hDparent := parentSlice65.1
  have parentSlice66 := parentSlice65.2
  have hIntertwineParent := parentSlice66.1
  have hGlobal := parentSlice66.2
  let A : HP →L[ℝ] HP := HP.orthogonalProjectionOnto ∘L U.toContinuousLinearMap ∘L HP.subtypeL
  let B : HP →L[ℝ] Lp ℝ 2 J :=
    (((1 : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J)-P)*U.toContinuousLinearMap*P) ∘L HP.subtypeL
  let ΓP : HP →L[ℝ] HP := e.conjStarAlgEquiv Γ
  let qP : HP := e q
  let HP0 := (innerSL ℝ qP).ker
  letI : NormedAddCommGroup HP0 := HP0.normedAddCommGroup
  letI : InnerProductSpace ℝ HP0 := HP0.innerProductSpace
  letI : CompleteSpace HP0 := (innerSL ℝ qP).isClosed_ker.completeSpace_coe
  let Hperp := P.ker
  letI : NormedAddCommGroup Hperp := Hperp.normedAddCommGroup
  letI : InnerProductSpace ℝ Hperp := Hperp.innerProductSpace
  letI : CompleteSpace Hperp := P.isClosed_ker.completeSpace_coe
  change HP0 →L[ℝ] Hperp at B0 V0
  change HP0 →L[ℝ] HP0 at ΓP0 Inv A0
  change Lp ℝ 2 J →L[ℝ] Hperp at R
  change (∀ g : Lp ℝ 2 J, (R g : Lp ℝ 2 J)=g-P g) at hR
  change (∀ g : Lp ℝ 2 J,
    B.adjoint g=HP0.subtypeL (B0.adjoint (R g))) at hAmbient
  change (∀ f : Lp ℝ 2 J, (∫ z, f z ∂J)=0 →
    ∃ fP : HP0,
      HP0.subtypeL fP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le f ∧
      let fperp : Hperp := R f
      let fV : HP0 := V0.adjoint fperp
      B.adjoint (fperp : Lp ℝ 2 J)=HP0.subtypeL (ΓP0 fV) ∧
      HP0.subtypeL (ΓP0 fV)=ΓP (HP0.subtypeL fV) ∧
      ‖f‖^2=‖fP‖^2+‖fperp‖^2 ∧ ‖fV‖≤‖fperp‖) at hGlobal

Exact compiled BODY span; preceding local definitions and inherited Hilbert structures stay in scope.

2. Prove mean preservation from the actual law

The current U acts almost everywhere by the actual reflection F. The independently compiled augmentation invariance gives F#J=J, so change of variables preserves the integral. Conditional expectation preserves the full integral as well. Since J is a probability law, every L2 observable is integrable, and subtraction of actual representatives is legitimate.

\[F_\#J=J,\quad\int Uu\,dJ=\int u\,dJ,\quad\int Pu\,dJ=\int u\,dJ,\quad L^2(J)\subset L^1(J).\]
Corresponding Lean step
  let D : Hperp →L[ℝ] Hperp := R ∘L U.toContinuousLinearMap ∘L Hperp.subtypeL
  have hD (h : Hperp) : (D h : Lp ℝ 2 J)=
      U (h : Lp ℝ 2 J)-P (U (h : Lp ℝ 2 J)) := hDparent h
  have hIntertwine : V0.adjoint ∘L D= -(A0 ∘L V0.adjoint) := hIntertwineParent
  letI : IsProbabilityMeasure μ := hμ
  letI : IsProbabilityMeasure J := hJ
  let F : E × E → E × E := fun z => (z.1,(2 : ℝ) • z.1-z.2)
  have hFmeas : Measurable F := by fun_prop
  have hFJ : Measure.map F J=J :=
    (AutoSamplingTheory.ExampleCases.ProximalBPS.GaussianReflection.reflection_preserves_augmentation μ η hη).2
  have hUIntegral (u : Lp ℝ 2 J) : (∫ z, U u z ∂J)=∫ z, u z ∂J := by
    calc
      (∫ z, U u z ∂J)=(∫ z, u (F z) ∂J) := integral_congr_ae (hU u)
      _ = (∫ z, u z ∂Measure.map F J) :=
        (integral_map hFmeas.aemeasurable (by rw [hFJ]; exact (Lp.memLp u).aestronglyMeasurable)).symm
      _ = (∫ z, u z ∂J) := by rw [hFJ]
  have hPIntegral (u : Lp ℝ 2 J) : (∫ z, P u z ∂J)=∫ z, u z ∂J := by
    change (∫ z, (condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le u : E × E → ℝ) z ∂J)=_
    simpa only [Measure.restrict_univ] using
      (integral_condExpL2_eq (𝕜:=ℝ) (s:=Set.univ) measurable_snd.comap_le u
        MeasurableSet.univ (measure_ne_top J Set.univ))
  have hIntegrable (u : Lp ℝ 2 J) : Integrable u J :=
    MemLp.integrable (by norm_num : (1 : ℝ≥0∞) ≤ 2) (Lp.memLp u)
  have hSubIntegral (u v : Lp ℝ 2 J) :
      (∫ z, (u-v) z ∂J)=(∫ z, u z ∂J)-(∫ z, v z ∂J) :=
    (integral_congr_ae (Lp.coeFn_sub u v)).trans (integral_sub (hIntegrable u) (hIntegrable v))
  have hPself : IsSelfAdjoint P := isSelfAdjoint_starProjection HP

Exact compiled BODY span; preceding local definitions and inherited Hilbert structures stay in scope.

3. Identify actual macro and micro compressions

Include the centered macro space into the joint L2 space by iota. Orthogonality to ker P follows from selfadjointness of P. The same A0 and B0 split the reflected macro vector. The actual residual and polar-adjoint identities then identify its micro component without any range or surjectivity premise.

\[PU\iota u=\iota A_0u,\quad U\iota u=\iota A_0u+i_\perp B_0u,\quad RU\iota u=B_0u,\quad V_0^*B_0u=\Gamma_0u.\]
Corresponding Lean step
  let ι : HP0 →L[ℝ] Lp ℝ 2 J := HP.subtypeL ∘L HP0.subtypeL
  have hPι (u : HP0) : P (ι u)=ι u := hPf (u : HP)
  have hOrth (u : HP0) (h : Hperp) : inner ℝ (ι u) (h : Lp ℝ 2 J)=0 := by
    calc
      inner ℝ (ι u) (h : Lp ℝ 2 J)=inner ℝ (P (ι u)) (h : Lp ℝ 2 J) := by rw [hPι]
      _ = inner ℝ (ι u) (P (h : Lp ℝ 2 J)) := hPself.isSymmetric _ _
      _ = 0 := by rw [show P (h : Lp ℝ 2 J)=0 from h.property,inner_zero_right]
  have hMacro (u : HP0) : P (U (ι u))=ι (A0 u) := by
    change (A (u : HP) : Lp ℝ 2 J)=((A0 u : HP) : Lp ℝ 2 J)
    exact congrArg (fun x : HP => (x : Lp ℝ 2 J)) (hA0 u).symm
  have hMicro (u : HP0) : (B0 u : Lp ℝ 2 J)=U (ι u)-P (U (ι u)) := by
    rw [hB0]
    change U (P (ι u))-P (U (P (ι u)))=U (ι u)-P (U (ι u))
    rw [hPι]
  have hUι (u : HP0) : U (ι u)=ι (A0 u)+(B0 u : Lp ℝ 2 J) := by
    rw [hMicro,←hMacro]
    abel
  have hRmicro (h : Hperp) : R (h : Lp ℝ 2 J)=h := by
    apply Subtype.ext
    rw [hR,show P (h : Lp ℝ 2 J)=0 from h.property,sub_zero]
  have hRUm (u : HP0) : R (U (ι u))=B0 u := by
    apply Subtype.ext
    rw [hR]
    exact (hMicro u).symm
  have hVadjB (u : HP0) : V0.adjoint (B0 u)=ΓP0 u := by
    have hb := DFunLike.congr_fun hFactor u
    change B0 u=V0 (ΓP0 u) at hb
    rw [hb]
    exact DFunLike.congr_fun hVadj (ΓP0 u)

Exact compiled BODY span; preceding local definitions and inherited Hilbert structures stay in scope.

4. Obtain the scalar energy and cross-term identities

Positivity makes Gamma0 selfadjoint; A0 is selfadjoint already. Test A0^2+Gamma0^2=I against u to get the scalar norm identity. Move A0 and Gamma0 across the inner products and use their commutation to identify the two mixed terms.

\[\|A_0u\|^2+\|\Gamma_0u\|^2=\|u\|^2,\qquad\langle A_0u,\Gamma_0v\rangle=\langle\Gamma_0u,A_0v\rangle.\]
Corresponding Lean step
  have hΓself : IsSelfAdjoint ΓP0 := (show ΓP0.IsPositive from hPos0).isSelfAdjoint
  have hEnergy (u : HP0) : ‖A0 u‖^2+‖ΓP0 u‖^2=‖u‖^2 := by
    have h := congrArg (fun L : HP0 →L[ℝ] HP0 => inner ℝ (L u) u) hSquare0
    simp only [ContinuousLinearMap.add_apply,ContinuousLinearMap.mul_apply,
      ContinuousLinearMap.one_apply,inner_add_left] at h
    have ha : inner ℝ (A0 (A0 u)) u=‖A0 u‖^2 :=
      (hA0self.isSymmetric (A0 u) u).trans (real_inner_self_eq_norm_sq _)
    have hg : inner ℝ (ΓP0 (ΓP0 u)) u=‖ΓP0 u‖^2 :=
      (hΓself.isSymmetric (ΓP0 u) u).trans (real_inner_self_eq_norm_sq _)
    rw [ha,hg,real_inner_self_eq_norm_sq] at h
    exact h
  have hCross (u v : HP0) : inner ℝ (A0 u) (ΓP0 v)=inner ℝ (ΓP0 u) (A0 v) := by
    calc
      inner ℝ (A0 u) (ΓP0 v)=inner ℝ u (A0 (ΓP0 v)) := hA0self.isSymmetric _ _
      _ = inner ℝ u (ΓP0 (A0 v)) := congrArg (fun z : HP0 => inner ℝ u z) (DFunLike.congr_fun hComm0.eq v)
      _ = inner ℝ (ΓP0 u) (A0 v) := (hΓself.isSymmetric _ _).symm

Exact compiled BODY span; preceding local definitions and inherited Hilbert structures stay in scope.

5. Produce the components of the actual reflected input

Start with an arbitrary globally centered f. Obtain fP from the same actual conditional expectation and fV=V0*Rf. Define g by the actual U action. Integral preservation gives mean(g)=mean(f)-[mean(f)-mean(f)]=0, so the SAME existing producer applies to g and supplies its actual gP. No zero-output-mean premise or RHS-defined component is used.

\[f_\perp=Rf,\ f_V=V_0^*f_\perp,\ g=U(\iota f_P-i_\perp f_\perp),\quad\int g\,dJ=0,\quad\iota g_P=Pg.\]
Corresponding Lean step
  have hGlobal70 :
      (∀ f : Lp ℝ 2 J, (∫ z, f z ∂J)=0 →
                            ∃ fP : HP0,
                              HP0.subtypeL fP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le f ∧
                              let fperp : Hperp := R f
                              let fV : HP0 := V0.adjoint fperp
                              B.adjoint (fperp : Lp ℝ 2 J)=HP0.subtypeL (ΓP0 fV) ∧
                              HP0.subtypeL (ΓP0 fV)=ΓP (HP0.subtypeL fV) ∧
                              ‖f‖^2=‖fP‖^2+‖fperp‖^2 ∧ ‖fV‖≤‖fperp‖ ∧
                              let g : Lp ℝ 2 J := U (P f-(f-P f))
                              (∫ z, g z ∂J)=0 ∧
                              ∃ gP : HP0,
                                HP0.subtypeL gP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le g ∧
                                let gperp : Hperp := R g
                                let gV : HP0 := V0.adjoint gperp
                                gP=A0 fP-ΓP0 fV ∧
                                gV=ΓP0 fP+A0 fV ∧
                                ‖gP‖^2+‖gV‖^2=‖fP‖^2+‖fV‖^2) := by
    intro f hf
    obtain ⟨fP,hfP,hBf,hΓf,hBudget,hVBudget⟩ := hGlobal f hf
    let fperp : Hperp := R f
    let fV : HP0 := V0.adjoint fperp
    change B.adjoint (fperp : Lp ℝ 2 J)=HP0.subtypeL (ΓP0 fV) at hBf
    have hPfp : P f=ι fP :=
      (congrArg (fun x : HP => (x : Lp ℝ 2 J)) hfP).symm
    have hB0adjMicro : B0.adjoint fperp=ΓP0 fV := by
      apply Subtype.ext
      have h := (hAmbient (fperp : Lp ℝ 2 J)).symm.trans hBf
      rw [hRmicro] at h
      exact h
    let g : Lp ℝ 2 J := U (P f-(f-P f))
    have hgMean : (∫ z, g z ∂J)=0 := by
      change (∫ z, U (P f-(f-P f)) z ∂J)=0
      rw [hUIntegral]
      simp only [hSubIntegral,hPIntegral,hf,sub_self]
    obtain ⟨gP,hgP,hgtail⟩ := hGlobal g hgMean
    have hPgp : P g=ι gP :=
      (congrArg (fun x : HP => (x : Lp ℝ 2 J)) hgP).symm
    have hInput : P f-(f-P f)=ι fP-(fperp : Lp ℝ 2 J) := by
      change P f-(f-P f)=ι fP-(R f : Lp ℝ 2 J)
      rw [hR f,hPfp]

Exact compiled BODY span; preceding local definitions and inherited Hilbert structures stay in scope.

6. Derive the actual macro rotation by inner-product separation

For every centered macro test vector u, move P and U across the inner product using selfadjointness. Split U iota u into its actual macro/micro components; the cross-subspace terms vanish by orthogonality. The adjoint relation B0* fperp=Gamma0 fV and selfadjoint A0 identify the remaining terms. Separation identifies the already produced gP.

\[\langle u,g_P\rangle=\langle U\iota u,\iota f_P-i_\perp f_\perp\rangle=\langle A_0u,f_P\rangle-\langle B_0u,f_\perp\rangle=\langle u,A_0f_P-\Gamma_0f_V\rangle.\]
Corresponding Lean step
    have hgPformula : gP=A0 fP-ΓP0 fV := by
      apply ext_inner_left ℝ
      intro u
      calc
        inner ℝ u gP=inner ℝ (ι u) (ι gP) := rfl
        _ = inner ℝ (ι u) (P g) := by rw [hPgp]
        _ = inner ℝ (P (ι u)) g := (hPself.isSymmetric _ _).symm
        _ = inner ℝ (ι u) g := by rw [hPι]
        _ = inner ℝ (U (ι u)) (ι fP-(fperp : Lp ℝ 2 J)) := by
          change inner ℝ (ι u) (U (P f-(f-P f)))=_
          rw [hInput]
          exact (hUs.isSymmetric _ _).symm
        _ = inner ℝ (A0 u) fP-inner ℝ (B0 u) fperp := by
          rw [hUι,inner_add_left,inner_sub_right,inner_sub_right,
            hOrth (A0 u) fperp,
            show inner ℝ (B0 u : Lp ℝ 2 J) (ι fP)=0 from
              (real_inner_comm _ _).trans (hOrth fP (B0 u))]
          change (inner ℝ (A0 u) fP-0)+(0-inner ℝ (B0 u) fperp)=_
          ring
        _ = inner ℝ u (A0 fP)-inner ℝ u (ΓP0 fV) := by
          have ha : inner ℝ (A0 u) fP=inner ℝ u (A0 fP) := hA0self.isSymmetric u fP
          have hb : inner ℝ (B0 u) fperp=inner ℝ u (ΓP0 fV) :=
            (B0.adjoint_inner_right u fperp).symm.trans
              (congrArg (fun z : HP0 => inner ℝ u z) hB0adjMicro)
          exact congrArg₂ (fun x y : ℝ => x-y) ha hb
        _ = inner ℝ u (A0 fP-ΓP0 fV) := (inner_sub_right _ _ _).symm

Exact compiled BODY span; preceding local definitions and inherited Hilbert structures stay in scope.

7. Derive the actual polar rotation on the full micro space

Linearity of U,R and V0* gives the reflected macro contribution Gamma0 fP minus the reflected micro contribution V0*D fperp. Apply the full-domain intertwining identity to this actual fperp in ker P. This yields the formula for gV=V0*Rg on its actual output semantics.

\[g_V=V_0^*RU\iota f_P-V_0^*D f_\perp=\Gamma_0f_P+A_0V_0^*f_\perp=\Gamma_0f_P+A_0f_V.\]
Corresponding Lean step
    have hgVformula : V0.adjoint (R g)=ΓP0 fP+A0 fV := by
      change V0.adjoint (R (U (P f-(f-P f))))=_
      rw [hInput,map_sub,map_sub,hRUm,map_sub,hVadjB]
      have hd := DFunLike.congr_fun hIntertwine fperp
      change V0.adjoint (D fperp)= -(A0 fV) at hd
      change ΓP0 fP-V0.adjoint (D fperp)=_
      rw [hd,sub_neg_eq_add]

Exact compiled BODY span; preceding local definitions and inherited Hilbert structures stay in scope.

8. Cancel mixed terms and retain every original witness

Expand the squared norms of the two formulas. The opposite mixed terms cancel by the cross-term identity, and the two scalar energy identities reduce the remaining sum to the input pair energy. Reassemble the complete original proposition with the same twelve witnesses. This is the projected rotation ingredient consumed by the subsequent actual B21 corrector change, not the remaining dynamics or main sampling theorem.

\[\|A_0f_P-\Gamma_0f_V\|^2+\|\Gamma_0f_P+A_0f_V\|^2=\|A_0f_P\|^2+\|\Gamma_0f_P\|^2+\|A_0f_V\|^2+\|\Gamma_0f_V\|^2=\|f_P\|^2+\|f_V\|^2.\]
Corresponding Lean step
    have hgEnergy : ‖gP‖^2+‖V0.adjoint (R g)‖^2=‖fP‖^2+‖fV‖^2 := by
      rw [hgPformula,hgVformula,norm_sub_sq_real,norm_add_sq_real,hCross]
      nlinarith only [hEnergy fP,hEnergy fV]
    exact ⟨fP,hfP,hBf,hΓf,hBudget,hVBudget,hgMean,gP,hgP,hgPformula,hgVformula,hgEnergy⟩
  have hFinal :
      (∀ h : Hperp, (D h : Lp ℝ 2 J)=U (h : Lp ℝ 2 J)-P (U (h : Lp ℝ 2 J))) ∧
      V0.adjoint ∘L D= -(A0 ∘L V0.adjoint) ∧
      (∀ f : Lp ℝ 2 J, (∫ z, f z ∂J)=0 →
                            ∃ fP : HP0,
                              HP0.subtypeL fP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le f ∧
                              let fperp : Hperp := R f
                              let fV : HP0 := V0.adjoint fperp
                              B.adjoint (fperp : Lp ℝ 2 J)=HP0.subtypeL (ΓP0 fV) ∧
                              HP0.subtypeL (ΓP0 fV)=ΓP (HP0.subtypeL fV) ∧
                              ‖f‖^2=‖fP‖^2+‖fperp‖^2 ∧ ‖fV‖≤‖fperp‖ ∧
                              let g : Lp ℝ 2 J := U (P f-(f-P f))
                              (∫ z, g z ∂J)=0 ∧
                              ∃ gP : HP0,
                                HP0.subtypeL gP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le g ∧
                                let gperp : Hperp := R g
                                let gV : HP0 := V0.adjoint gperp
                                gP=A0 fP-ΓP0 fV ∧
                                gV=ΓP0 fP+A0 fV ∧
                                ‖gP‖^2+‖gV‖^2=‖fP‖^2+‖fV‖^2) := ⟨hD,hIntertwine,hGlobal70⟩
  refine ⟨hμ, ?_⟩
  refine ⟨hJ, ?_⟩
  refine ⟨hν, ?_⟩
  refine ⟨hRange, ?_⟩
  refine ⟨hPf, ?_⟩
  refine ⟨S, ?_⟩
  refine ⟨hS, ?_⟩
  refine ⟨hSd, ?_⟩
  refine ⟨hSc, ?_⟩
  refine ⟨hSf, ?_⟩
  refine ⟨hSs, ?_⟩
  refine ⟨e, ?_⟩
  refine ⟨he, ?_⟩
  refine ⟨U, ?_⟩
  refine ⟨hU, ?_⟩
  refine ⟨hUi, ?_⟩
  refine ⟨hUs, ?_⟩
  refine ⟨T, ?_⟩
  refine ⟨hTs, ?_⟩
  refine ⟨hAll, ?_⟩
  refine ⟨hAeq, ?_⟩
  refine ⟨hAs, ?_⟩
  refine ⟨hAn, ?_⟩
  refine ⟨hPB, ?_⟩
  refine ⟨Γ, ?_⟩
  refine ⟨hΓ, ?_⟩
  refine ⟨hΓSq, ?_⟩
  refine ⟨hCommRoot, ?_⟩
  refine ⟨hΓP, ?_⟩
  refine ⟨hΓPSq, ?_⟩
  refine ⟨hCommP, ?_⟩
  refine ⟨hGram, ?_⟩
  refine ⟨q, ?_⟩
  refine ⟨hqa, ?_⟩
  refine ⟨hTq, ?_⟩
  refine ⟨hq, ?_⟩
  refine ⟨hCenter, ?_⟩
  refine ⟨hΓPq, ?_⟩
  refine ⟨hγ, ?_⟩
  refine ⟨ΓP0, ?_⟩
  refine ⟨hΓP0, ?_⟩
  refine ⟨hPos0, ?_⟩
  refine ⟨hOrder0, ?_⟩
  refine ⟨hUnit, ?_⟩
  refine ⟨Inv, ?_⟩
  refine ⟨hLeft, ?_⟩
  refine ⟨hRight, ?_⟩
  refine ⟨hNormInv, ?_⟩
  refine ⟨hInvSelf,A0,hA0,hA0self,hComm0,hSquare0,hCommInv,?_⟩
  refine ⟨B0, ?_⟩
  refine ⟨hB0, ?_⟩
  refine ⟨V0, ?_⟩
  refine ⟨hVdef, ?_⟩
  refine ⟨hFactor, ?_⟩
  refine ⟨hVadj, ?_⟩
  refine ⟨hVnorm, ?_⟩
  refine ⟨R, ?_⟩
  refine ⟨hR, ?_⟩
  refine ⟨hAmbient, ?_⟩
  exact hFinal

Exact compiled BODY span; preceding local definitions and inherited Hilbert structures stay in scope.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · actual_projected_rotation

Retain the same actual probability geometry and operators; Prove mean preservation from the actual law; Identify actual macro and micro compressions; Obtain the scalar energy and cross-term identities; Produce the components of the actual reflected input; Derive the actual macro rotation by inner-product separation; Derive the actual polar rotation on the full micro space; Cancel mixed terms and retain every original witness

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
theorem actual_projected_rotation
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ)*‖v‖^2)
    (hη : 0 < η) (hβη : (β : ℝ)*η ≤ 1) : actual_projected_rotation_statement (E:=E) (V:=V) (α:=α) (β:=β) (η:=η) hα hαβ hV hH hη hβη := by
  unfold actual_projected_rotation_statement
  classical
  let μ := (volume : Measure E).tilted (fun x => -V x)
  let J := (μ.prod (stdGaussian E)).map
    (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
  let ν := J.snd
  let mY : MeasurableSpace (E × E) := MeasurableSpace.comap Prod.snd (inferInstance : MeasurableSpace E)
  letI : MeasurableSpace (E × E) := Prod.instMeasurableSpace
  letI : Fact (mY ≤ (inferInstance : MeasurableSpace (E × E))) := ⟨measurable_snd.comap_le⟩
  let HP := lpMeas ℝ ℝ mY 2 J
  letI : NormedAddCommGroup HP := HP.normedAddCommGroup
  letI : InnerProductSpace ℝ HP := HP.innerProductSpace
  let P : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J :=
    HP.subtypeL ∘L condExpL2 ℝ ℝ (μ := J) measurable_snd.comap_le
  have hBase := AutoSamplingTheory.ExampleCases.ProximalBPS.ReflectionIntertwining.actual_reflection_intertwining
    (E:=E) (V:=V) (α:=α) (β:=β) (η:=η) hα hαβ hV hH hη hβη
  have parentSlice0 := hBase
  have hμ := parentSlice0.1
  have parentSlice1 := parentSlice0.2
  have hJ := parentSlice1.1
  have parentSlice2 := parentSlice1.2
  have hν := parentSlice2.1
  have parentSlice3 := parentSlice2.2
  have hRange := parentSlice3.1
  have parentSlice4 := parentSlice3.2
  have hPf := parentSlice4.1
  have parentSlice5 := parentSlice4.2
  obtain ⟨S, parentSlice6⟩ := parentSlice5
  have hS := parentSlice6.1
  have parentSlice7 := parentSlice6.2
  have hSd := parentSlice7.1
  have parentSlice8 := parentSlice7.2
  have hSc := parentSlice8.1
  have parentSlice9 := parentSlice8.2
  have hSf := parentSlice9.1
  have parentSlice10 := parentSlice9.2
  have hSs := parentSlice10.1
  have parentSlice11 := parentSlice10.2
  obtain ⟨e, parentSlice12⟩ := parentSlice11
  have he := parentSlice12.1
  have parentSlice13 := parentSlice12.2
  obtain ⟨U, parentSlice14⟩ := parentSlice13
  have hU := parentSlice14.1
  have parentSlice15 := parentSlice14.2
  have hUi := parentSlice15.1
  have parentSlice16 := parentSlice15.2
  have hUs := parentSlice16.1
  have parentSlice17 := parentSlice16.2
  obtain ⟨T, parentSlice18⟩ := parentSlice17
  have hTs := parentSlice18.1
  have parentSlice19 := parentSlice18.2
  have hAll := parentSlice19.1
  have parentSlice20 := parentSlice19.2
  have hAeq := parentSlice20.1
  have parentSlice21 := parentSlice20.2
  have hAs := parentSlice21.1
  have parentSlice22 := parentSlice21.2
  have hAn := parentSlice22.1
  have parentSlice23 := parentSlice22.2
  have hPB := parentSlice23.1
  have parentSlice24 := parentSlice23.2
  obtain ⟨Γ, parentSlice25⟩ := parentSlice24
  have hΓ := parentSlice25.1
  have parentSlice26 := parentSlice25.2
  have hΓSq := parentSlice26.1
  have parentSlice27 := parentSlice26.2
  have hCommRoot := parentSlice27.1
  have parentSlice28 := parentSlice27.2
  have hΓP := parentSlice28.1
  have parentSlice29 := parentSlice28.2
  have hΓPSq := parentSlice29.1
  have parentSlice30 := parentSlice29.2
  have hCommP := parentSlice30.1
  have parentSlice31 := parentSlice30.2
  have hGram := parentSlice31.1
  have parentSlice32 := parentSlice31.2
  obtain ⟨q, parentSlice33⟩ := parentSlice32
  have hqa := parentSlice33.1
  have parentSlice34 := parentSlice33.2
  have hTq := parentSlice34.1
  have parentSlice35 := parentSlice34.2
  have hq := parentSlice35.1
  have parentSlice36 := parentSlice35.2
  have hCenter := parentSlice36.1
  have parentSlice37 := parentSlice36.2
  have hΓPq := parentSlice37.1
  have parentSlice38 := parentSlice37.2
  have hγ := parentSlice38.1
  have parentSlice39 := parentSlice38.2
  obtain ⟨ΓP0, parentSlice40⟩ := parentSlice39
  have hΓP0 := parentSlice40.1
  have parentSlice41 := parentSlice40.2
  have hPos0 := parentSlice41.1
  have parentSlice42 := parentSlice41.2
  have hOrder0 := parentSlice42.1
  have parentSlice43 := parentSlice42.2
  have hUnit := parentSlice43.1
  have parentSlice44 := parentSlice43.2
  obtain ⟨Inv, parentSlice45⟩ := parentSlice44
  have hLeft := parentSlice45.1
  have parentSlice46 := parentSlice45.2
  have hRight := parentSlice46.1
  have parentSlice47 := parentSlice46.2
  have hNormInv := parentSlice47.1
  have parentSlice48 := parentSlice47.2
  have hInvSelf := parentSlice48.1
  have parentSlice49 := parentSlice48.2
  obtain ⟨A0, parentSlice50⟩ := parentSlice49
  have hA0 := parentSlice50.1
  have parentSlice51 := parentSlice50.2
  have hA0self := parentSlice51.1
  have parentSlice52 := parentSlice51.2
  have hComm0 := parentSlice52.1
  have parentSlice53 := parentSlice52.2
  have hSquare0 := parentSlice53.1
  have parentSlice54 := parentSlice53.2
  have hCommInv := parentSlice54.1
  have parentSlice55 := parentSlice54.2
  obtain ⟨B0, parentSlice56⟩ := parentSlice55
  have hB0 := parentSlice56.1
  have parentSlice57 := parentSlice56.2
  obtain ⟨V0, parentSlice58⟩ := parentSlice57
  have hVdef := parentSlice58.1
  have parentSlice59 := parentSlice58.2
  have hFactor := parentSlice59.1
  have parentSlice60 := parentSlice59.2
  have hVadj := parentSlice60.1
  have parentSlice61 := parentSlice60.2
  have hVnorm := parentSlice61.1
  have parentSlice62 := parentSlice61.2
  obtain ⟨R, parentSlice63⟩ := parentSlice62
  have hR := parentSlice63.1
  have parentSlice64 := parentSlice63.2
  have hAmbient := parentSlice64.1
  have parentSlice65 := parentSlice64.2
  have hDparent := parentSlice65.1
  have parentSlice66 := parentSlice65.2
  have hIntertwineParent := parentSlice66.1
  have hGlobal := parentSlice66.2
  let A : HP →L[ℝ] HP := HP.orthogonalProjectionOnto ∘L U.toContinuousLinearMap ∘L HP.subtypeL
  let B : HP →L[ℝ] Lp ℝ 2 J :=
    (((1 : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J)-P)*U.toContinuousLinearMap*P) ∘L HP.subtypeL
  let ΓP : HP →L[ℝ] HP := e.conjStarAlgEquiv Γ
  let qP : HP := e q
  let HP0 := (innerSL ℝ qP).ker
  letI : NormedAddCommGroup HP0 := HP0.normedAddCommGroup
  letI : InnerProductSpace ℝ HP0 := HP0.innerProductSpace
  letI : CompleteSpace HP0 := (innerSL ℝ qP).isClosed_ker.completeSpace_coe
  let Hperp := P.ker
  letI : NormedAddCommGroup Hperp := Hperp.normedAddCommGroup
  letI : InnerProductSpace ℝ Hperp := Hperp.innerProductSpace
  letI : CompleteSpace Hperp := P.isClosed_ker.completeSpace_coe
  change HP0 →L[ℝ] Hperp at B0 V0
  change HP0 →L[ℝ] HP0 at ΓP0 Inv A0
  change Lp ℝ 2 J →L[ℝ] Hperp at R
  change (∀ g : Lp ℝ 2 J, (R g : Lp ℝ 2 J)=g-P g) at hR
  change (∀ g : Lp ℝ 2 J,
    B.adjoint g=HP0.subtypeL (B0.adjoint (R g))) at hAmbient
  change (∀ f : Lp ℝ 2 J, (∫ z, f z ∂J)=0 →
    ∃ fP : HP0,
      HP0.subtypeL fP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le f ∧
      let fperp : Hperp := R f
      let fV : HP0 := V0.adjoint fperp
      B.adjoint (fperp : Lp ℝ 2 J)=HP0.subtypeL (ΓP0 fV) ∧
      HP0.subtypeL (ΓP0 fV)=ΓP (HP0.subtypeL fV) ∧
      ‖f‖^2=‖fP‖^2+‖fperp‖^2 ∧ ‖fV‖≤‖fperp‖) at hGlobal
  let D : Hperp →L[ℝ] Hperp := R ∘L U.toContinuousLinearMap ∘L Hperp.subtypeL
  have hD (h : Hperp) : (D h : Lp ℝ 2 J)=
      U (h : Lp ℝ 2 J)-P (U (h : Lp ℝ 2 J)) := hDparent h
  have hIntertwine : V0.adjoint ∘L D= -(A0 ∘L V0.adjoint) := hIntertwineParent
  letI : IsProbabilityMeasure μ := hμ
  letI : IsProbabilityMeasure J := hJ
  let F : E × E → E × E := fun z => (z.1,(2 : ℝ) • z.1-z.2)
  have hFmeas : Measurable F := by fun_prop
  have hFJ : Measure.map F J=J :=
    (AutoSamplingTheory.ExampleCases.ProximalBPS.GaussianReflection.reflection_preserves_augmentation μ η hη).2
  have hUIntegral (u : Lp ℝ 2 J) : (∫ z, U u z ∂J)=∫ z, u z ∂J := by
    calc
      (∫ z, U u z ∂J)=(∫ z, u (F z) ∂J) := integral_congr_ae (hU u)
      _ = (∫ z, u z ∂Measure.map F J) :=
        (integral_map hFmeas.aemeasurable (by rw [hFJ]; exact (Lp.memLp u).aestronglyMeasurable)).symm
      _ = (∫ z, u z ∂J) := by rw [hFJ]
  have hPIntegral (u : Lp ℝ 2 J) : (∫ z, P u z ∂J)=∫ z, u z ∂J := by
    change (∫ z, (condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le u : E × E → ℝ) z ∂J)=_
    simpa only [Measure.restrict_univ] using
      (integral_condExpL2_eq (𝕜:=ℝ) (s:=Set.univ) measurable_snd.comap_le u
        MeasurableSet.univ (measure_ne_top J Set.univ))
  have hIntegrable (u : Lp ℝ 2 J) : Integrable u J :=
    MemLp.integrable (by norm_num : (1 : ℝ≥0∞) ≤ 2) (Lp.memLp u)
  have hSubIntegral (u v : Lp ℝ 2 J) :
      (∫ z, (u-v) z ∂J)=(∫ z, u z ∂J)-(∫ z, v z ∂J) :=
    (integral_congr_ae (Lp.coeFn_sub u v)).trans (integral_sub (hIntegrable u) (hIntegrable v))
  have hPself : IsSelfAdjoint P := isSelfAdjoint_starProjection HP
  let ι : HP0 →L[ℝ] Lp ℝ 2 J := HP.subtypeL ∘L HP0.subtypeL
  have hPι (u : HP0) : P (ι u)=ι u := hPf (u : HP)
  have hOrth (u : HP0) (h : Hperp) : inner ℝ (ι u) (h : Lp ℝ 2 J)=0 := by
    calc
      inner ℝ (ι u) (h : Lp ℝ 2 J)=inner ℝ (P (ι u)) (h : Lp ℝ 2 J) := by rw [hPι]
      _ = inner ℝ (ι u) (P (h : Lp ℝ 2 J)) := hPself.isSymmetric _ _
      _ = 0 := by rw [show P (h : Lp ℝ 2 J)=0 from h.property,inner_zero_right]
  have hMacro (u : HP0) : P (U (ι u))=ι (A0 u) := by
    change (A (u : HP) : Lp ℝ 2 J)=((A0 u : HP) : Lp ℝ 2 J)
    exact congrArg (fun x : HP => (x : Lp ℝ 2 J)) (hA0 u).symm
  have hMicro (u : HP0) : (B0 u : Lp ℝ 2 J)=U (ι u)-P (U (ι u)) := by
    rw [hB0]
    change U (P (ι u))-P (U (P (ι u)))=U (ι u)-P (U (ι u))
    rw [hPι]
  have hUι (u : HP0) : U (ι u)=ι (A0 u)+(B0 u : Lp ℝ 2 J) := by
    rw [hMicro,←hMacro]
    abel
  have hRmicro (h : Hperp) : R (h : Lp ℝ 2 J)=h := by
    apply Subtype.ext
    rw [hR,show P (h : Lp ℝ 2 J)=0 from h.property,sub_zero]
  have hRUm (u : HP0) : R (U (ι u))=B0 u := by
    apply Subtype.ext
    rw [hR]
    exact (hMicro u).symm
  have hVadjB (u : HP0) : V0.adjoint (B0 u)=ΓP0 u := by
    have hb := DFunLike.congr_fun hFactor u
    change B0 u=V0 (ΓP0 u) at hb
    rw [hb]
    exact DFunLike.congr_fun hVadj (ΓP0 u)
  have hΓself : IsSelfAdjoint ΓP0 := (show ΓP0.IsPositive from hPos0).isSelfAdjoint
  have hEnergy (u : HP0) : ‖A0 u‖^2+‖ΓP0 u‖^2=‖u‖^2 := by
    have h := congrArg (fun L : HP0 →L[ℝ] HP0 => inner ℝ (L u) u) hSquare0
    simp only [ContinuousLinearMap.add_apply,ContinuousLinearMap.mul_apply,
      ContinuousLinearMap.one_apply,inner_add_left] at h
    have ha : inner ℝ (A0 (A0 u)) u=‖A0 u‖^2 :=
      (hA0self.isSymmetric (A0 u) u).trans (real_inner_self_eq_norm_sq _)
    have hg : inner ℝ (ΓP0 (ΓP0 u)) u=‖ΓP0 u‖^2 :=
      (hΓself.isSymmetric (ΓP0 u) u).trans (real_inner_self_eq_norm_sq _)
    rw [ha,hg,real_inner_self_eq_norm_sq] at h
    exact h
  have hCross (u v : HP0) : inner ℝ (A0 u) (ΓP0 v)=inner ℝ (ΓP0 u) (A0 v) := by
    calc
      inner ℝ (A0 u) (ΓP0 v)=inner ℝ u (A0 (ΓP0 v)) := hA0self.isSymmetric _ _
      _ = inner ℝ u (ΓP0 (A0 v)) := congrArg (fun z : HP0 => inner ℝ u z) (DFunLike.congr_fun hComm0.eq v)
      _ = inner ℝ (ΓP0 u) (A0 v) := (hΓself.isSymmetric _ _).symm
  have hGlobal70 :
      (∀ f : Lp ℝ 2 J, (∫ z, f z ∂J)=0 →
                            ∃ fP : HP0,
                              HP0.subtypeL fP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le f ∧
                              let fperp : Hperp := R f
                              let fV : HP0 := V0.adjoint fperp
                              B.adjoint (fperp : Lp ℝ 2 J)=HP0.subtypeL (ΓP0 fV) ∧
                              HP0.subtypeL (ΓP0 fV)=ΓP (HP0.subtypeL fV) ∧
                              ‖f‖^2=‖fP‖^2+‖fperp‖^2 ∧ ‖fV‖≤‖fperp‖ ∧
                              let g : Lp ℝ 2 J := U (P f-(f-P f))
                              (∫ z, g z ∂J)=0 ∧
                              ∃ gP : HP0,
                                HP0.subtypeL gP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le g ∧
                                let gperp : Hperp := R g
                                let gV : HP0 := V0.adjoint gperp
                                gP=A0 fP-ΓP0 fV ∧
                                gV=ΓP0 fP+A0 fV ∧
                                ‖gP‖^2+‖gV‖^2=‖fP‖^2+‖fV‖^2) := by
    intro f hf
    obtain ⟨fP,hfP,hBf,hΓf,hBudget,hVBudget⟩ := hGlobal f hf
    let fperp : Hperp := R f
    let fV : HP0 := V0.adjoint fperp
    change B.adjoint (fperp : Lp ℝ 2 J)=HP0.subtypeL (ΓP0 fV) at hBf
    have hPfp : P f=ι fP :=
      (congrArg (fun x : HP => (x : Lp ℝ 2 J)) hfP).symm
    have hB0adjMicro : B0.adjoint fperp=ΓP0 fV := by
      apply Subtype.ext
      have h := (hAmbient (fperp : Lp ℝ 2 J)).symm.trans hBf
      rw [hRmicro] at h
      exact h
    let g : Lp ℝ 2 J := U (P f-(f-P f))
    have hgMean : (∫ z, g z ∂J)=0 := by
      change (∫ z, U (P f-(f-P f)) z ∂J)=0
      rw [hUIntegral]
      simp only [hSubIntegral,hPIntegral,hf,sub_self]
    obtain ⟨gP,hgP,hgtail⟩ := hGlobal g hgMean
    have hPgp : P g=ι gP :=
      (congrArg (fun x : HP => (x : Lp ℝ 2 J)) hgP).symm
    have hInput : P f-(f-P f)=ι fP-(fperp : Lp ℝ 2 J) := by
      change P f-(f-P f)=ι fP-(R f : Lp ℝ 2 J)
      rw [hR f,hPfp]
    have hgPformula : gP=A0 fP-ΓP0 fV := by
      apply ext_inner_left ℝ
      intro u
      calc
        inner ℝ u gP=inner ℝ (ι u) (ι gP) := rfl
        _ = inner ℝ (ι u) (P g) := by rw [hPgp]
        _ = inner ℝ (P (ι u)) g := (hPself.isSymmetric _ _).symm
        _ = inner ℝ (ι u) g := by rw [hPι]
        _ = inner ℝ (U (ι u)) (ι fP-(fperp : Lp ℝ 2 J)) := by
          change inner ℝ (ι u) (U (P f-(f-P f)))=_
          rw [hInput]
          exact (hUs.isSymmetric _ _).symm
        _ = inner ℝ (A0 u) fP-inner ℝ (B0 u) fperp := by
          rw [hUι,inner_add_left,inner_sub_right,inner_sub_right,
            hOrth (A0 u) fperp,
            show inner ℝ (B0 u : Lp ℝ 2 J) (ι fP)=0 from
              (real_inner_comm _ _).trans (hOrth fP (B0 u))]
          change (inner ℝ (A0 u) fP-0)+(0-inner ℝ (B0 u) fperp)=_
          ring
        _ = inner ℝ u (A0 fP)-inner ℝ u (ΓP0 fV) := by
          have ha : inner ℝ (A0 u) fP=inner ℝ u (A0 fP) := hA0self.isSymmetric u fP
          have hb : inner ℝ (B0 u) fperp=inner ℝ u (ΓP0 fV) :=
            (B0.adjoint_inner_right u fperp).symm.trans
              (congrArg (fun z : HP0 => inner ℝ u z) hB0adjMicro)
          exact congrArg₂ (fun x y : ℝ => x-y) ha hb
        _ = inner ℝ u (A0 fP-ΓP0 fV) := (inner_sub_right _ _ _).symm
    have hgVformula : V0.adjoint (R g)=ΓP0 fP+A0 fV := by
      change V0.adjoint (R (U (P f-(f-P f))))=_
      rw [hInput,map_sub,map_sub,hRUm,map_sub,hVadjB]
      have hd := DFunLike.congr_fun hIntertwine fperp
      change V0.adjoint (D fperp)= -(A0 fV) at hd
      change ΓP0 fP-V0.adjoint (D fperp)=_
      rw [hd,sub_neg_eq_add]
    have hgEnergy : ‖gP‖^2+‖V0.adjoint (R g)‖^2=‖fP‖^2+‖fV‖^2 := by
      rw [hgPformula,hgVformula,norm_sub_sq_real,norm_add_sq_real,hCross]
      nlinarith only [hEnergy fP,hEnergy fV]
    exact ⟨fP,hfP,hBf,hΓf,hBudget,hVBudget,hgMean,gP,hgP,hgPformula,hgVformula,hgEnergy⟩
  have hFinal :
      (∀ h : Hperp, (D h : Lp ℝ 2 J)=U (h : Lp ℝ 2 J)-P (U (h : Lp ℝ 2 J))) ∧
      V0.adjoint ∘L D= -(A0 ∘L V0.adjoint) ∧
      (∀ f : Lp ℝ 2 J, (∫ z, f z ∂J)=0 →
                            ∃ fP : HP0,
                              HP0.subtypeL fP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le f ∧
                              let fperp : Hperp := R f
                              let fV : HP0 := V0.adjoint fperp
                              B.adjoint (fperp : Lp ℝ 2 J)=HP0.subtypeL (ΓP0 fV) ∧
                              HP0.subtypeL (ΓP0 fV)=ΓP (HP0.subtypeL fV) ∧
                              ‖f‖^2=‖fP‖^2+‖fperp‖^2 ∧ ‖fV‖≤‖fperp‖ ∧
                              let g : Lp ℝ 2 J := U (P f-(f-P f))
                              (∫ z, g z ∂J)=0 ∧
                              ∃ gP : HP0,
                                HP0.subtypeL gP=condExpL2 ℝ ℝ (μ:=J) measurable_snd.comap_le g ∧
                                let gperp : Hperp := R g
                                let gV : HP0 := V0.adjoint gperp
                                gP=A0 fP-ΓP0 fV ∧
                                gV=ΓP0 fP+A0 fV ∧
                                ‖gP‖^2+‖gV‖^2=‖fP‖^2+‖fV‖^2) := ⟨hD,hIntertwine,hGlobal70⟩
  refine ⟨hμ, ?_⟩
  refine ⟨hJ, ?_⟩
  refine ⟨hν, ?_⟩
  refine ⟨hRange, ?_⟩
  refine ⟨hPf, ?_⟩
  refine ⟨S, ?_⟩
  refine ⟨hS, ?_⟩
  refine ⟨hSd, ?_⟩
  refine ⟨hSc, ?_⟩
  refine ⟨hSf, ?_⟩
  refine ⟨hSs, ?_⟩
  refine ⟨e, ?_⟩
  refine ⟨he, ?_⟩
  refine ⟨U, ?_⟩
  refine ⟨hU, ?_⟩
  refine ⟨hUi, ?_⟩
  refine ⟨hUs, ?_⟩
  refine ⟨T, ?_⟩
  refine ⟨hTs, ?_⟩
  refine ⟨hAll, ?_⟩
  refine ⟨hAeq, ?_⟩
  refine ⟨hAs, ?_⟩
  refine ⟨hAn, ?_⟩
  refine ⟨hPB, ?_⟩
  refine ⟨Γ, ?_⟩
  refine ⟨hΓ, ?_⟩
  refine ⟨hΓSq, ?_⟩
  refine ⟨hCommRoot, ?_⟩
  refine ⟨hΓP, ?_⟩
  refine ⟨hΓPSq, ?_⟩
  refine ⟨hCommP, ?_⟩
  refine ⟨hGram, ?_⟩
  refine ⟨q, ?_⟩
  refine ⟨hqa, ?_⟩
  refine ⟨hTq, ?_⟩
  refine ⟨hq, ?_⟩
  refine ⟨hCenter, ?_⟩
  refine ⟨hΓPq, ?_⟩
  refine ⟨hγ, ?_⟩
  refine ⟨ΓP0, ?_⟩
  refine ⟨hΓP0, ?_⟩
  refine ⟨hPos0, ?_⟩
  refine ⟨hOrder0, ?_⟩
  refine ⟨hUnit, ?_⟩
  refine ⟨Inv, ?_⟩
  refine ⟨hLeft, ?_⟩
  refine ⟨hRight, ?_⟩
  refine ⟨hNormInv, ?_⟩
  refine ⟨hInvSelf,A0,hA0,hA0self,hComm0,hSquare0,hCommInv,?_⟩
  refine ⟨B0, ?_⟩
  refine ⟨hB0, ?_⟩
  refine ⟨V0, ?_⟩
  refine ⟨hVdef, ?_⟩
  refine ⟨hFactor, ?_⟩
  refine ⟨hVadj, ?_⟩
  refine ⟨hVnorm, ?_⟩
  refine ⟨R, ?_⟩
  refine ⟨hR, ?_⟩
  refine ⟨hAmbient, ?_⟩
  exact hFinal

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualProjectedRotation

#print axioms AutoSamplingTheory.ExampleCases.ProximalBPS.ActualProjectedRotation.actual_projected_rotation

Exact module and namespace context

Scope and omitted-condition boundaries
  • P16 same corrector algebra and actual B21 change remain next; B4/H1/dynamics/main/errors/cost/composition independent.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • MeasureTheory.integral_map
  • MeasureTheory.integral_condExpL2_eq
  • MeasureTheory.MemLp.integrable
  • MeasureTheory.Lp.coeFn_sub
  • ContinuousLinearMap.adjoint_inner_right
  • IsSelfAdjoint.isSymmetric
  • Commute.eq
  • norm_add_sq_real
  • norm_sub_sq_real

Mathematical sources

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.