Bounded Borel functions on the plane

def CommutingRepetition.BorelCalc.Bdd2 (F : ℝ × ℝ → ℝ) : Prop

Bounded measurable real functions on ℝ².

Equations

• CommutingRepetition.BorelCalc.Bdd2 F = (Measurable F ∧ ∃ (C : ℝ), ∀ (p : ℝ × ℝ), |F p| ≤ C)

theorem CommutingRepetition.BorelCalc.Bdd2.measurable {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) : Measurable F

theorem CommutingRepetition.BorelCalc.Bdd2.integrable {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (μ : MeasureTheory.Measure (ℝ × ℝ)) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Integrable F μ

theorem CommutingRepetition.BorelCalc.Bdd2.const (c : ℝ) : Bdd2 fun (x : ℝ × ℝ) => c

theorem CommutingRepetition.BorelCalc.Bdd2.one : Bdd2 1

theorem CommutingRepetition.BorelCalc.Bdd2.zero : Bdd2 0

theorem CommutingRepetition.BorelCalc.Bdd2.add {F G : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hG : Bdd2 G) : Bdd2 (F + G)

theorem CommutingRepetition.BorelCalc.Bdd2.neg {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) : Bdd2 (-F)

theorem CommutingRepetition.BorelCalc.Bdd2.sub {F G : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hG : Bdd2 G) : Bdd2 (F - G)

theorem CommutingRepetition.BorelCalc.Bdd2.mul {F G : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hG : Bdd2 G) : Bdd2 (F * G)

theorem CommutingRepetition.BorelCalc.Bdd2.const_mul {F : ℝ × ℝ → ℝ} (c : ℝ) (hF : Bdd2 F) : Bdd2 fun (p : ℝ × ℝ) => c * F p

theorem CommutingRepetition.BorelCalc.Bdd2.of_continuous {F : ℝ × ℝ → ℝ} (hF : Continuous F) {C : ℝ} (hC : ∀ (p : ℝ × ℝ), |F p| ≤ C) : Bdd2 F

theorem CommutingRepetition.BorelCalc.Bdd2.comp_fst {g : ℝ → ℝ} (hg : Bdd g) : Bdd2 fun (p : ℝ × ℝ) => g p.1

theorem CommutingRepetition.BorelCalc.Bdd2.comp_snd {g : ℝ → ℝ} (hg : Bdd g) : Bdd2 fun (p : ℝ × ℝ) => g p.2

theorem CommutingRepetition.BorelCalc.Bdd2.comp {F : ℝ × ℝ → ℝ} {g : ℝ → ℝ} (hg : Bdd g) (hF : Measurable F) : Bdd2 fun (p : ℝ × ℝ) => g (F p)

theorem CommutingRepetition.BorelCalc.Bdd2.max_zero {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) : Bdd2 fun (p : ℝ × ℝ) => max (F p) 0

theorem CommutingRepetition.BorelCalc.Bdd2.of_compactlySupported (f : CompactlySupportedContinuousMap (ℝ × ℝ) ℝ) : Bdd2 ⇑f

Combinations of finite measures on the plane and the transfer principle

def CommutingRepetition.BorelCalc.IsCombo2 (Φ : (ℝ × ℝ → ℝ) → ℂ) : Prop

Φ is a combination of four finite measures on ℝ².

Equations

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

theorem CommutingRepetition.BorelCalc.IsCombo2.integral (μ : MeasureTheory.Measure (ℝ × ℝ)) [MeasureTheory.IsFiniteMeasure μ] : IsCombo2 fun (F : ℝ × ℝ → ℝ) => ↑(∫ (p : ℝ × ℝ), F p ∂μ)

theorem CommutingRepetition.BorelCalc.IsCombo2.congr {Φ Ψ : (ℝ × ℝ → ℝ) → ℂ} (hΦ : IsCombo2 Φ) (h : ∀ (F : ℝ × ℝ → ℝ), Bdd2 F → Φ F = Ψ F) : IsCombo2 Ψ

theorem CommutingRepetition.BorelCalc.IsCombo2.add {Φ Ψ : (ℝ × ℝ → ℝ) → ℂ} (hΦ : IsCombo2 Φ) (hΨ : IsCombo2 Ψ) : IsCombo2 fun (F : ℝ × ℝ → ℝ) => Φ F + Ψ F

theorem CommutingRepetition.BorelCalc.IsCombo2.smul_real (r : ℝ) {Φ : (ℝ × ℝ → ℝ) → ℂ} (hΦ : IsCombo2 Φ) : IsCombo2 fun (F : ℝ × ℝ → ℝ) => ↑r * Φ F

theorem CommutingRepetition.BorelCalc.IsCombo2.smul_I {Φ : (ℝ × ℝ → ℝ) → ℂ} (hΦ : IsCombo2 Φ) : IsCombo2 fun (F : ℝ × ℝ → ℝ) => Complex.I * Φ F

theorem CommutingRepetition.BorelCalc.IsCombo2.smul (c : ℂ) {Φ : (ℝ × ℝ → ℝ) → ℂ} (hΦ : IsCombo2 Φ) : IsCombo2 fun (F : ℝ × ℝ → ℝ) => c * Φ F

theorem CommutingRepetition.BorelCalc.IsCombo2.neg {Φ : (ℝ × ℝ → ℝ) → ℂ} (hΦ : IsCombo2 Φ) : IsCombo2 fun (F : ℝ × ℝ → ℝ) => -Φ F

theorem CommutingRepetition.BorelCalc.IsCombo2.sub {Φ Ψ : (ℝ × ℝ → ℝ) → ℂ} (hΦ : IsCombo2 Φ) (hΨ : IsCombo2 Ψ) : IsCombo2 fun (F : ℝ × ℝ → ℝ) => Φ F - Ψ F

theorem CommutingRepetition.BorelCalc.IsCombo2.conjugate {Φ : (ℝ × ℝ → ℝ) → ℂ} (hΦ : IsCombo2 Φ) : IsCombo2 fun (F : ℝ × ℝ → ℝ) => (starRingEnd ℂ) (Φ F)

theorem CommutingRepetition.BorelCalc.IsCombo2.transfer {Φ : (ℝ × ℝ → ℝ) → ℂ} (hΦ : IsCombo2 Φ) (h : ∀ (F : ℝ × ℝ → ℝ), Continuous F → Bdd2 F → Φ F = 0) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) : Φ F = 0

Transfer principle on the plane: a combination vanishing on all compactly supported continuous functions vanishes on all bounded Borel functions.

theorem CommutingRepetition.BorelCalc.IsCombo2.eq {Φ Ψ : (ℝ × ℝ → ℝ) → ℂ} (hΦ : IsCombo2 Φ) (hΨ : IsCombo2 Ψ) (h : ∀ (F : ℝ × ℝ → ℝ), Continuous F → Bdd2 F → Φ F = Ψ F) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) : Φ F = Ψ F

Multiplying the test function by a fixed bounded Borel function

noncomputable def CommutingRepetition.BorelCalc.IsCombo2.wd2 (μ : MeasureTheory.Measure (ℝ × ℝ)) (H : ℝ × ℝ → ℝ) : MeasureTheory.Measure (ℝ × ℝ)

The measure H⁺ dμ.

Equations

• CommutingRepetition.BorelCalc.IsCombo2.wd2 μ H = μ.withDensity fun (p : ℝ × ℝ) => ↑(H p).toNNReal

theorem CommutingRepetition.BorelCalc.IsCombo2.wd2_isFiniteMeasure (μ : MeasureTheory.Measure (ℝ × ℝ)) [MeasureTheory.IsFiniteMeasure μ] {H : ℝ × ℝ → ℝ} (hH : Bdd2 H) : MeasureTheory.IsFiniteMeasure (wd2 μ H)

theorem CommutingRepetition.BorelCalc.IsCombo2.integral_wd2 (μ : MeasureTheory.Measure (ℝ × ℝ)) {H : ℝ × ℝ → ℝ} (hH : Bdd2 H) (F : ℝ × ℝ → ℝ) : ∫ (p : ℝ × ℝ), F p ∂wd2 μ H = ∫ (p : ℝ × ℝ), max (H p) 0 * F p ∂μ

theorem CommutingRepetition.BorelCalc.IsCombo2.integral_mul_eq_wd2 (μ : MeasureTheory.Measure (ℝ × ℝ)) [MeasureTheory.IsFiniteMeasure μ] {F H : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hH : Bdd2 H) : ∫ (p : ℝ × ℝ), (F * H) p ∂μ = ∫ (p : ℝ × ℝ), F p ∂wd2 μ H - ∫ (p : ℝ × ℝ), F p ∂wd2 μ (-H)

theorem CommutingRepetition.BorelCalc.IsCombo2.mul_right {Φ : (ℝ × ℝ → ℝ) → ℂ} (hΦ : IsCombo2 Φ) {H : ℝ × ℝ → ℝ} (hH : Bdd2 H) : IsCombo2 fun (F : ℝ × ℝ → ℝ) => Φ (F * H)

theorem CommutingRepetition.BorelCalc.IsCombo2.mul_left {Φ : (ℝ × ℝ → ℝ) → ℂ} (hΦ : IsCombo2 Φ) {H : ℝ × ℝ → ℝ} (hH : Bdd2 H) : IsCombo2 fun (F : ℝ × ℝ → ℝ) => Φ (H * F)

The polarized form and the joint calculus

def CommutingRepetition.BorelCalc.Fc (F : ℝ × ℝ → ℝ) (z : ℂ) : ℂ

A real function on the plane, read as a function of a complex variable.

Equations

• CommutingRepetition.BorelCalc.Fc F z = ↑(F (z.re, z.im))

theorem CommutingRepetition.BorelCalc.continuous_Fc {F : ℝ × ℝ → ℝ} (hF : Continuous F) : Continuous (Fc F)

theorem CommutingRepetition.BorelCalc.cfc_Fc_isSelfAdjoint {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (F : ℝ × ℝ → ℝ) : IsSelfAdjoint (cfc (Fc F) (Zp E₁ E₂))

noncomputable def CommutingRepetition.BorelCalc.Q2 {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) (F : ℝ × ℝ → ℝ) (ξ : 𝓗) : ℂ

The quadratic form Q2 F ξ = ∫ F dνP_ξ.

Equations

• CommutingRepetition.BorelCalc.Q2 E₁ E₂ h₁ h₂ hc F ξ = ↑(∫ (p : ℝ × ℝ), F p ∂CommutingRepetition.BorelCalc.νP E₁ E₂ h₁ h₂ hc ξ)

noncomputable def CommutingRepetition.BorelCalc.pol2 {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) (F : ℝ × ℝ → ℝ) (ξ η : 𝓗) : ℂ

The polarized form.

Equations

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

theorem CommutingRepetition.BorelCalc.isCombo2_Q2 {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) (ξ : 𝓗) : IsCombo2 fun (F : ℝ × ℝ → ℝ) => Q2 E₁ E₂ h₁ h₂ hc F ξ

theorem CommutingRepetition.BorelCalc.isCombo2_pol2 {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) (ξ η : 𝓗) : IsCombo2 fun (F : ℝ × ℝ → ℝ) => pol2 E₁ E₂ h₁ h₂ hc F ξ η

theorem CommutingRepetition.BorelCalc.Q2_cfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Continuous F) (ξ : 𝓗) : Q2 E₁ E₂ h₁ h₂ hc F ξ = inner ℂ ξ ((cfc (Fc F) (Zp E₁ E₂)) ξ)

theorem CommutingRepetition.BorelCalc.pol2_cfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Continuous F) (ξ η : 𝓗) : pol2 E₁ E₂ h₁ h₂ hc F ξ η = inner ℂ ξ ((cfc (Fc F) (Zp E₁ E₂)) η)

theorem CommutingRepetition.BorelCalc.pol2_add_left {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (ξ ξ' η : 𝓗) : pol2 E₁ E₂ h₁ h₂ hc F (ξ + ξ') η = pol2 E₁ E₂ h₁ h₂ hc F ξ η + pol2 E₁ E₂ h₁ h₂ hc F ξ' η

theorem CommutingRepetition.BorelCalc.pol2_smul_left {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (c : ℂ) (ξ η : 𝓗) : pol2 E₁ E₂ h₁ h₂ hc F (c • ξ) η = (starRingEnd ℂ) c * pol2 E₁ E₂ h₁ h₂ hc F ξ η

theorem CommutingRepetition.BorelCalc.pol2_add_right {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (ξ η η' : 𝓗) : pol2 E₁ E₂ h₁ h₂ hc F ξ (η + η') = pol2 E₁ E₂ h₁ h₂ hc F ξ η + pol2 E₁ E₂ h₁ h₂ hc F ξ η'

theorem CommutingRepetition.BorelCalc.pol2_smul_right {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (c : ℂ) (ξ η : 𝓗) : pol2 E₁ E₂ h₁ h₂ hc F ξ (c • η) = c * pol2 E₁ E₂ h₁ h₂ hc F ξ η

theorem CommutingRepetition.BorelCalc.pol2_conj {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (ξ η : 𝓗) : (starRingEnd ℂ) (pol2 E₁ E₂ h₁ h₂ hc F η ξ) = pol2 E₁ E₂ h₁ h₂ hc F ξ η

theorem CommutingRepetition.BorelCalc.pol2_self {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (ξ : 𝓗) : pol2 E₁ E₂ h₁ h₂ hc F ξ ξ = Q2 E₁ E₂ h₁ h₂ hc F ξ

theorem CommutingRepetition.BorelCalc.pol2_zero_left {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (η : 𝓗) : pol2 E₁ E₂ h₁ h₂ hc F 0 η = 0

theorem CommutingRepetition.BorelCalc.pol2_zero_right {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (ξ : 𝓗) : pol2 E₁ E₂ h₁ h₂ hc F ξ 0 = 0

Boundedness

theorem CommutingRepetition.BorelCalc.norm_Q2_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} {C : ℝ} (hC : ∀ (p : ℝ × ℝ), |F p| ≤ C) (ξ : 𝓗) : ‖Q2 E₁ E₂ h₁ h₂ hc F ξ‖ ≤ C * ‖ξ‖ ^ 2

theorem CommutingRepetition.BorelCalc.norm_pol2_le_sq {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} {C : ℝ} (hC : ∀ (p : ℝ × ℝ), |F p| ≤ C) (ξ η : 𝓗) : ‖pol2 E₁ E₂ h₁ h₂ hc F ξ η‖ ≤ C * (‖ξ‖ ^ 2 + ‖η‖ ^ 2)

theorem CommutingRepetition.BorelCalc.norm_pol2_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) {C : ℝ} (hC : ∀ (p : ℝ × ℝ), |F p| ≤ C) (ξ η : 𝓗) : ‖pol2 E₁ E₂ h₁ h₂ hc F ξ η‖ ≤ 2 * C * ‖ξ‖ * ‖η‖

noncomputable def CommutingRepetition.BorelCalc.polForm2 {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) : 𝓗 →L⋆[ℂ] 𝓗 →L[ℂ] ℂ

The polarized form as a bounded sesquilinear map.

Equations

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

theorem CommutingRepetition.BorelCalc.polForm2_apply {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (ξ η : 𝓗) : ((polForm2 E₁ E₂ h₁ h₂ hc hF) ξ) η = pol2 E₁ E₂ h₁ h₂ hc F ξ η

The joint Borel functional calculus

noncomputable def CommutingRepetition.BorelCalc.jbfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) (F : ℝ × ℝ → ℝ) : 𝓗 →L[ℂ] 𝓗

The joint Borel functional calculus F(E₁, E₂) for a bounded Borel F : ℝ² → ℝ (junk value 0 otherwise).

Equations

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

theorem CommutingRepetition.BorelCalc.jbfc_of_not {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : ¬Bdd2 F) : jbfc E₁ E₂ h₁ h₂ hc F = 0

theorem CommutingRepetition.BorelCalc.inner_jbfc_left {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (ξ η : 𝓗) : inner ℂ ((jbfc E₁ E₂ h₁ h₂ hc F) ξ) η = pol2 E₁ E₂ h₁ h₂ hc F ξ η

theorem CommutingRepetition.BorelCalc.inner_jbfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (ξ η : 𝓗) : inner ℂ ξ ((jbfc E₁ E₂ h₁ h₂ hc F) η) = pol2 E₁ E₂ h₁ h₂ hc F ξ η

theorem CommutingRepetition.BorelCalc.inner_jbfc_self {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (ξ : 𝓗) : inner ℂ ξ ((jbfc E₁ E₂ h₁ h₂ hc F) ξ) = Q2 E₁ E₂ h₁ h₂ hc F ξ

theorem CommutingRepetition.BorelCalc.re_inner_jbfc_self {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (ξ : 𝓗) : (inner ℂ ξ ((jbfc E₁ E₂ h₁ h₂ hc F) ξ)).re = ∫ (p : ℝ × ℝ), F p ∂νP E₁ E₂ h₁ h₂ hc ξ

theorem CommutingRepetition.BorelCalc.jbfc_unique {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) {T : 𝓗 →L[ℂ] 𝓗} (h : ∀ (ξ η : 𝓗), inner ℂ ξ (T η) = pol2 E₁ E₂ h₁ h₂ hc F ξ η) : T = jbfc E₁ E₂ h₁ h₂ hc F

theorem CommutingRepetition.BorelCalc.jbfc_cfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hFc : Continuous F) : jbfc E₁ E₂ h₁ h₂ hc F = cfc (Fc F) (Zp E₁ E₂)

On bounded continuous functions the joint calculus is the continuous calculus of Z = E₁ + i E₂.

theorem CommutingRepetition.BorelCalc.jbfc_isSelfAdjoint {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) : IsSelfAdjoint (jbfc E₁ E₂ h₁ h₂ hc F)

One-variable functions

theorem CommutingRepetition.BorelCalc.Q2_comp_fst {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {g : ℝ → ℝ} (hg : Bdd g) (ξ : 𝓗) : Q2 E₁ E₂ h₁ h₂ hc (fun (p : ℝ × ℝ) => g p.1) ξ = Q E₁ h₁ g ξ

theorem CommutingRepetition.BorelCalc.Q2_comp_snd {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {g : ℝ → ℝ} (hg : Bdd g) (ξ : 𝓗) : Q2 E₁ E₂ h₁ h₂ hc (fun (p : ℝ × ℝ) => g p.2) ξ = Q E₂ h₂ g ξ

theorem CommutingRepetition.BorelCalc.pol2_comp_fst {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {g : ℝ → ℝ} (hg : Bdd g) (ξ η : 𝓗) : pol2 E₁ E₂ h₁ h₂ hc (fun (p : ℝ × ℝ) => g p.1) ξ η = pol E₁ h₁ g ξ η

theorem CommutingRepetition.BorelCalc.pol2_comp_snd {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {g : ℝ → ℝ} (hg : Bdd g) (ξ η : 𝓗) : pol2 E₁ E₂ h₁ h₂ hc (fun (p : ℝ × ℝ) => g p.2) ξ η = pol E₂ h₂ g ξ η

theorem CommutingRepetition.BorelCalc.jbfc_fst {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {g : ℝ → ℝ} (hg : Bdd g) : (jbfc E₁ E₂ h₁ h₂ hc fun (p : ℝ × ℝ) => g p.1) = bfc E₁ h₁ g

theorem CommutingRepetition.BorelCalc.jbfc_snd {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {g : ℝ → ℝ} (hg : Bdd g) : (jbfc E₁ E₂ h₁ h₂ hc fun (p : ℝ × ℝ) => g p.2) = bfc E₂ h₂ g

Linearity

theorem CommutingRepetition.BorelCalc.Q2_add {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F G : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hG : Bdd2 G) (ξ : 𝓗) : Q2 E₁ E₂ h₁ h₂ hc (F + G) ξ = Q2 E₁ E₂ h₁ h₂ hc F ξ + Q2 E₁ E₂ h₁ h₂ hc G ξ

theorem CommutingRepetition.BorelCalc.Q2_sub {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F G : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hG : Bdd2 G) (ξ : 𝓗) : Q2 E₁ E₂ h₁ h₂ hc (F - G) ξ = Q2 E₁ E₂ h₁ h₂ hc F ξ - Q2 E₁ E₂ h₁ h₂ hc G ξ

theorem CommutingRepetition.BorelCalc.Q2_const_mul {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) (c : ℝ) (F : ℝ × ℝ → ℝ) (ξ : 𝓗) : Q2 E₁ E₂ h₁ h₂ hc (fun (p : ℝ × ℝ) => c * F p) ξ = ↑c * Q2 E₁ E₂ h₁ h₂ hc F ξ

theorem CommutingRepetition.BorelCalc.pol2_add_fun {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F G : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hG : Bdd2 G) (ξ η : 𝓗) : pol2 E₁ E₂ h₁ h₂ hc (F + G) ξ η = pol2 E₁ E₂ h₁ h₂ hc F ξ η + pol2 E₁ E₂ h₁ h₂ hc G ξ η

theorem CommutingRepetition.BorelCalc.pol2_sub_fun {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F G : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hG : Bdd2 G) (ξ η : 𝓗) : pol2 E₁ E₂ h₁ h₂ hc (F - G) ξ η = pol2 E₁ E₂ h₁ h₂ hc F ξ η - pol2 E₁ E₂ h₁ h₂ hc G ξ η

theorem CommutingRepetition.BorelCalc.pol2_const_mul {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) (c : ℝ) (F : ℝ × ℝ → ℝ) (ξ η : 𝓗) : pol2 E₁ E₂ h₁ h₂ hc (fun (p : ℝ × ℝ) => c * F p) ξ η = ↑c * pol2 E₁ E₂ h₁ h₂ hc F ξ η

theorem CommutingRepetition.BorelCalc.jbfc_add {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F G : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hG : Bdd2 G) : jbfc E₁ E₂ h₁ h₂ hc (F + G) = jbfc E₁ E₂ h₁ h₂ hc F + jbfc E₁ E₂ h₁ h₂ hc G

theorem CommutingRepetition.BorelCalc.jbfc_sub {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F G : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hG : Bdd2 G) : jbfc E₁ E₂ h₁ h₂ hc (F - G) = jbfc E₁ E₂ h₁ h₂ hc F - jbfc E₁ E₂ h₁ h₂ hc G

theorem CommutingRepetition.BorelCalc.jbfc_const_mul {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) (c : ℝ) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) : (jbfc E₁ E₂ h₁ h₂ hc fun (p : ℝ × ℝ) => c * F p) = ↑c • jbfc E₁ E₂ h₁ h₂ hc F

theorem CommutingRepetition.BorelCalc.jbfc_one {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) : jbfc E₁ E₂ h₁ h₂ hc 1 = 1

theorem CommutingRepetition.BorelCalc.jbfc_zero {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) : jbfc E₁ E₂ h₁ h₂ hc 0 = 0

theorem CommutingRepetition.BorelCalc.jbfc_const {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) (c : ℝ) : (jbfc E₁ E₂ h₁ h₂ hc fun (x : ℝ × ℝ) => c) = ↑c • 1

Multiplicativity

theorem CommutingRepetition.BorelCalc.cfc_Fc_mul {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) {F G : ℝ × ℝ → ℝ} (hF : Continuous F) (hG : Continuous G) : cfc (Fc (F * G)) (Zp E₁ E₂) = cfc (Fc F) (Zp E₁ E₂) * cfc (Fc G) (Zp E₁ E₂)

theorem CommutingRepetition.BorelCalc.pol2_jbfc_right_cont {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F G : ℝ × ℝ → ℝ} (hFc : Continuous F) (hF : Bdd2 F) (hG : Bdd2 G) (ξ η : 𝓗) : pol2 E₁ E₂ h₁ h₂ hc F ξ ((jbfc E₁ E₂ h₁ h₂ hc G) η) = pol2 E₁ E₂ h₁ h₂ hc (F * G) ξ η

Step 1: continuous F, Borel G (transfer in G).

theorem CommutingRepetition.BorelCalc.pol2_jbfc_right {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F G : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hG : Bdd2 G) (ξ η : 𝓗) : pol2 E₁ E₂ h₁ h₂ hc F ξ ((jbfc E₁ E₂ h₁ h₂ hc G) η) = pol2 E₁ E₂ h₁ h₂ hc (F * G) ξ η

Step 2: Borel F and G (transfer in F).

theorem CommutingRepetition.BorelCalc.jbfc_mul {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F G : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hG : Bdd2 G) : jbfc E₁ E₂ h₁ h₂ hc (F * G) = jbfc E₁ E₂ h₁ h₂ hc F * jbfc E₁ E₂ h₁ h₂ hc G

Multiplicativity of the joint Borel calculus.

theorem CommutingRepetition.BorelCalc.jbfc_comm {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F G : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hG : Bdd2 G) : jbfc E₁ E₂ h₁ h₂ hc F * jbfc E₁ E₂ h₁ h₂ hc G = jbfc E₁ E₂ h₁ h₂ hc G * jbfc E₁ E₂ h₁ h₂ hc F

Norms and order

theorem CommutingRepetition.BorelCalc.norm_sq_jbfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (ξ : 𝓗) : ‖(jbfc E₁ E₂ h₁ h₂ hc F) ξ‖ ^ 2 = ∫ (p : ℝ × ℝ), F p ^ 2 ∂νP E₁ E₂ h₁ h₂ hc ξ

‖F(E₁,E₂) ξ‖² = ∫ F² dνP_ξ.

theorem CommutingRepetition.BorelCalc.norm_jbfc_apply_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) {C : ℝ} (hC : ∀ (p : ℝ × ℝ), |F p| ≤ C) (ξ : 𝓗) : ‖(jbfc E₁ E₂ h₁ h₂ hc F) ξ‖ ≤ C * ‖ξ‖

theorem CommutingRepetition.BorelCalc.norm_jbfc_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) {C : ℝ} (hC : ∀ (p : ℝ × ℝ), |F p| ≤ C) : ‖jbfc E₁ E₂ h₁ h₂ hc F‖ ≤ C

theorem CommutingRepetition.BorelCalc.jbfc_nonneg {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (h0 : ∀ (p : ℝ × ℝ), 0 ≤ F p) : 0 ≤ jbfc E₁ E₂ h₁ h₂ hc F

theorem CommutingRepetition.BorelCalc.jbfc_mono {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F G : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hG : Bdd2 G) (hle : ∀ (p : ℝ × ℝ), F p ≤ G p) : jbfc E₁ E₂ h₁ h₂ hc F ≤ jbfc E₁ E₂ h₁ h₂ hc G

theorem CommutingRepetition.BorelCalc.tendsto_jbfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {ι : Type u_2} {l : Filter ι} [l.IsCountablyGenerated] {F : ι → ℝ × ℝ → ℝ} {Finf : ℝ × ℝ → ℝ} (hF : ∀ (i : ι), Bdd2 (F i)) (hFinf : Bdd2 Finf) {C : ℝ} (hC : ∀ (i : ι) (p : ℝ × ℝ), |F i p| ≤ C) (hCinf : ∀ (p : ℝ × ℝ), |Finf p| ≤ C) (hlim : ∀ (p : ℝ × ℝ), Filter.Tendsto (fun (i : ι) => F i p) l (nhds (Finf p))) (ξ : 𝓗) : Filter.Tendsto (fun (i : ι) => (jbfc E₁ E₂ h₁ h₂ hc (F i)) ξ) l (nhds ((jbfc E₁ E₂ h₁ h₂ hc Finf) ξ))

Dominated convergence: uniformly bounded F i → Finf pointwise gives F i (E₁,E₂) ξ → Finf (E₁,E₂) ξ.

Commutation and membership

theorem CommutingRepetition.BorelCalc.commute_Zp {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) {T : 𝓗 →L[ℂ] 𝓗} (hT₁ : Commute E₁ T) (hT₂ : Commute E₂ T) : Commute (Zp E₁ E₂) T

theorem CommutingRepetition.BorelCalc.commute_star_Zp {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) {T : 𝓗 →L[ℂ] 𝓗} (hT₁ : Commute E₁ T) (hT₂ : Commute E₂ T) : Commute (star (Zp E₁ E₂)) T

theorem CommutingRepetition.BorelCalc.commute_jbfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {T : 𝓗 →L[ℂ] 𝓗} (hT₁ : Commute E₁ T) (hT₂ : Commute E₂ T) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) : Commute (jbfc E₁ E₂ h₁ h₂ hc F) T

An operator commuting with E₁ and E₂ commutes with the joint calculus.

theorem CommutingRepetition.BorelCalc.jbfc_mem {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) (N : VonNeumannAlgebra 𝓗) (hE₁ : E₁ ∈ N) (hE₂ : E₂ ∈ N) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) : jbfc E₁ E₂ h₁ h₂ hc F ∈ N

The joint calculus of a pair in a von Neumann algebra stays in it.

Composition with a one-variable Borel function (continuous F)

theorem CommutingRepetition.BorelCalc.Q_jbfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hFc : Continuous F) {g : ℝ → ℝ} (hg : Bdd g) (ξ : 𝓗) : Q (jbfc E₁ E₂ h₁ h₂ hc F) ⋯ g ξ = Q2 E₁ E₂ h₁ h₂ hc (fun (p : ℝ × ℝ) => g (F p)) ξ

The spectral measure of F(E₁,E₂) at ξ is the pushforward of νP_ξ under F.

theorem CommutingRepetition.BorelCalc.bfc_jbfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hFc : Continuous F) {g : ℝ → ℝ} (hg : Bdd g) : bfc (jbfc E₁ E₂ h₁ h₂ hc F) ⋯ g = jbfc E₁ E₂ h₁ h₂ hc fun (p : ℝ × ℝ) => g (F p)

Composition: g(F(E₁,E₂)) = (g ∘ F)(E₁,E₂) for continuous bounded F and bounded Borel g.

theorem CommutingRepetition.BorelCalc.jbfc_congr_ae {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F G : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hG : Bdd2 G) (h : ∀ (ξ : 𝓗), F =ᵐ[νP E₁ E₂ h₁ h₂ hc ξ] G) : jbfc E₁ E₂ h₁ h₂ hc F = jbfc E₁ E₂ h₁ h₂ hc G

Almost-everywhere equal functions give the same operator.

Complex-valued functions

def CommutingRepetition.BorelCalc.CBdd2 (F : ℝ × ℝ → ℂ) : Prop

Bounded measurable complex functions on the plane.

Equations

• CommutingRepetition.BorelCalc.CBdd2 F = (Measurable F ∧ ∃ (C : ℝ), ∀ (p : ℝ × ℝ), ‖F p‖ ≤ C)

theorem CommutingRepetition.BorelCalc.CBdd2.re {F : ℝ × ℝ → ℂ} (hF : CBdd2 F) : Bdd2 fun (p : ℝ × ℝ) => (F p).re

theorem CommutingRepetition.BorelCalc.CBdd2.im {F : ℝ × ℝ → ℂ} (hF : CBdd2 F) : Bdd2 fun (p : ℝ × ℝ) => (F p).im

theorem CommutingRepetition.BorelCalc.CBdd2.ofReal {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) : CBdd2 fun (p : ℝ × ℝ) => ↑(F p)

theorem CommutingRepetition.BorelCalc.CBdd2.const (z : ℂ) : CBdd2 fun (x : ℝ × ℝ) => z

theorem CommutingRepetition.BorelCalc.CBdd2.add {F G : ℝ × ℝ → ℂ} (hF : CBdd2 F) (hG : CBdd2 G) : CBdd2 (F + G)

theorem CommutingRepetition.BorelCalc.CBdd2.mul {F G : ℝ × ℝ → ℂ} (hF : CBdd2 F) (hG : CBdd2 G) : CBdd2 (F * G)

theorem CommutingRepetition.BorelCalc.CBdd2.comp_fst {G : ℝ → ℂ} (hG : CBdd G) : CBdd2 fun (p : ℝ × ℝ) => G p.1

theorem CommutingRepetition.BorelCalc.CBdd2.comp_snd {G : ℝ → ℂ} (hG : CBdd G) : CBdd2 fun (p : ℝ × ℝ) => G p.2

theorem CommutingRepetition.BorelCalc.CBdd2.comp {G : ℝ → ℂ} (hG : CBdd G) {F : ℝ × ℝ → ℝ} (hF : Measurable F) : CBdd2 fun (p : ℝ × ℝ) => G (F p)

noncomputable def CommutingRepetition.BorelCalc.cjbfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) (F : ℝ × ℝ → ℂ) : 𝓗 →L[ℂ] 𝓗

The complex joint Borel calculus F(E₁,E₂) := (Re F)(E₁,E₂) + i (Im F)(E₁,E₂).

Equations

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

theorem CommutingRepetition.BorelCalc.cjbfc_ofReal {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) (F : ℝ × ℝ → ℝ) : (cjbfc E₁ E₂ h₁ h₂ hc fun (p : ℝ × ℝ) => ↑(F p)) = jbfc E₁ E₂ h₁ h₂ hc F

theorem CommutingRepetition.BorelCalc.cjbfc_fst {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {G : ℝ → ℂ} (hG : CBdd G) : (cjbfc E₁ E₂ h₁ h₂ hc fun (p : ℝ × ℝ) => G p.1) = cbfc E₁ h₁ G

theorem CommutingRepetition.BorelCalc.cjbfc_snd {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {G : ℝ → ℂ} (hG : CBdd G) : (cjbfc E₁ E₂ h₁ h₂ hc fun (p : ℝ × ℝ) => G p.2) = cbfc E₂ h₂ G

theorem CommutingRepetition.BorelCalc.cjbfc_add {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F G : ℝ × ℝ → ℂ} (hF : CBdd2 F) (hG : CBdd2 G) : cjbfc E₁ E₂ h₁ h₂ hc (F + G) = cjbfc E₁ E₂ h₁ h₂ hc F + cjbfc E₁ E₂ h₁ h₂ hc G

theorem CommutingRepetition.BorelCalc.cjbfc_mul {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F G : ℝ × ℝ → ℂ} (hF : CBdd2 F) (hG : CBdd2 G) : cjbfc E₁ E₂ h₁ h₂ hc (F * G) = cjbfc E₁ E₂ h₁ h₂ hc F * cjbfc E₁ E₂ h₁ h₂ hc G

theorem CommutingRepetition.BorelCalc.cjbfc_star {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℂ} (hF : CBdd2 F) : star (cjbfc E₁ E₂ h₁ h₂ hc F) = cjbfc E₁ E₂ h₁ h₂ hc fun (p : ℝ × ℝ) => (starRingEnd ℂ) (F p)

theorem CommutingRepetition.BorelCalc.cbfc_jbfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℝ} (hF : Bdd2 F) (hFc : Continuous F) {G : ℝ → ℂ} (hG : CBdd G) : cbfc (jbfc E₁ E₂ h₁ h₂ hc F) ⋯ G = cjbfc E₁ E₂ h₁ h₂ hc fun (p : ℝ × ℝ) => G (F p)

Composition for complex G: G(F(E₁,E₂)) = (G ∘ F)(E₁,E₂) (continuous bounded real F, bounded Borel G).

theorem CommutingRepetition.BorelCalc.commute_cjbfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {T : 𝓗 →L[ℂ] 𝓗} (hT₁ : Commute E₁ T) (hT₂ : Commute E₂ T) {F : ℝ × ℝ → ℂ} (hF : CBdd2 F) : Commute (cjbfc E₁ E₂ h₁ h₂ hc F) T

theorem CommutingRepetition.BorelCalc.cjbfc_mem {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) (N : VonNeumannAlgebra 𝓗) (hE₁ : E₁ ∈ N) (hE₂ : E₂ ∈ N) {F : ℝ × ℝ → ℂ} (hF : CBdd2 F) : cjbfc E₁ E₂ h₁ h₂ hc F ∈ N

theorem CommutingRepetition.BorelCalc.cjbfc_congr_ae {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F G : ℝ × ℝ → ℂ} (hF : CBdd2 F) (hG : CBdd2 G) (h : ∀ (ξ : 𝓗), F =ᵐ[νP E₁ E₂ h₁ h₂ hc ξ] G) : cjbfc E₁ E₂ h₁ h₂ hc F = cjbfc E₁ E₂ h₁ h₂ hc G

theorem CommutingRepetition.BorelCalc.norm_sq_cjbfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {F : ℝ × ℝ → ℂ} (hF : CBdd2 F) (ξ : 𝓗) : ‖(cjbfc E₁ E₂ h₁ h₂ hc F) ξ‖ ^ 2 = ∫ (p : ℝ × ℝ), ‖F p‖ ^ 2 ∂νP E₁ E₂ h₁ h₂ hc ξ

‖F(E₁,E₂) ξ‖² = ∫ |F|² dνP_ξ for complex F.