From 628b20fa427d2f6982838fae6a3a4486e1e115b9 Mon Sep 17 00:00:00 2001 From: Moritz Doll Date: Tue, 28 Jul 2026 11:17:30 +1000 Subject: [PATCH 1/2] stuff --- DynamicalSystems.lean | 2 +- DynamicalSystems/InputOutput/ClosedLoop.lean | 25 +++++ DynamicalSystems/InputOutput/Dissipative.lean | 53 ---------- DynamicalSystems/InputOutput/Passive.lean | 97 +++++++++++++++++++ 4 files changed, 123 insertions(+), 54 deletions(-) delete mode 100644 DynamicalSystems/InputOutput/Dissipative.lean create mode 100644 DynamicalSystems/InputOutput/Passive.lean diff --git a/DynamicalSystems.lean b/DynamicalSystems.lean index 831aa85..cf7a651 100644 --- a/DynamicalSystems.lean +++ b/DynamicalSystems.lean @@ -4,7 +4,7 @@ import DynamicalSystems.Basic.LpLoc import DynamicalSystems.Basic.NonAutonomous import DynamicalSystems.InputOutput.Causal import DynamicalSystems.InputOutput.ClosedLoop -import DynamicalSystems.InputOutput.Dissipative +import DynamicalSystems.InputOutput.Passive import DynamicalSystems.InputOutput.Example import DynamicalSystems.InputOutput.Stability import DynamicalSystems.Mathlib.Analysis.Calculus diff --git a/DynamicalSystems/InputOutput/ClosedLoop.lean b/DynamicalSystems/InputOutput/ClosedLoop.lean index 9aaac6a..295b310 100644 --- a/DynamicalSystems/InputOutput/ClosedLoop.lean +++ b/DynamicalSystems/InputOutput/ClosedLoop.lean @@ -6,6 +6,7 @@ Authors: Moritz Doll module public import DynamicalSystems.InputOutput.Stability +public import DynamicalSystems.InputOutput.Passive public import DynamicalSystems.Basic.WithLp public import Mathlib.Analysis.Normed.Lp.ProdLp @@ -635,6 +636,30 @@ theorem inputOutputLp_isFiniteGainStableWith [hp : Fact (1 ≤ p)] end IsFiniteGainStable +section IsPassiveWith + +variable [TopologicalSpace α] [InnerProductSpace ℝ E] + +variable {loop : SetRel.closedLoop α E E} {G₁ G₂ : (α → E) → α → E} + (hG₁ : G₁.graph = loop.topRel) (hG₁ : G₂.graph = loop.botRel) +--fun x y ↦ inner ℝ x y - δ • ‖x‖ ^ 2 - ε • ‖y‖ ^ 2 + +variable {ε₁ ε₂ δ₁ δ₂ β₁ β₂ : ℝ} +variable {s : ι → Set α} + +def passiveLoopBias : ℝ≥0 := sorry +def passiveLoopGain : ℝ≥0 := sorry + +theorem inputOutputLp_isFiniteGainStableWith' : + (loop.inputOutputLp 2).IsFiniteGainStableWith passiveLoopGain + passiveLoopBias s 2 μ := by + intro t e y he hy hey + rw [memLpLoc_withLp_prod_iff] at he hy + sorry + + +end IsPassiveWith + end SetRel.closedLoop variable (f : α → E × F) diff --git a/DynamicalSystems/InputOutput/Dissipative.lean b/DynamicalSystems/InputOutput/Dissipative.lean deleted file mode 100644 index fab54c4..0000000 --- a/DynamicalSystems/InputOutput/Dissipative.lean +++ /dev/null @@ -1,53 +0,0 @@ -/- -Copyright (c) 2026 Moritz Doll. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Moritz Doll --/ -module - -public import Mathlib.MeasureTheory.Function.LpSpace.Basic -public import Mathlib.MeasureTheory.Measure.Lebesgue.Basic -public import Mathlib.MeasureTheory.SpecificCodomains.Pi -public import DynamicalSystems.Mathlib.Analysis.ODE.GlobalExistence -public import DynamicalSystems.InputOutput.Causal - -/-! # Dissipative maps - --/ - -public section - -open MeasureTheory Filter Bornology Set -open scoped NNReal ENNReal - -variable {ι α 𝕜 E F G : Type*} - -variable [MeasurableSpace α] [Bornology α] - -variable (B : E → F → ℝ) {s : ι → Set α} - -/-- A map `f` is dissipative with bound `β` if for all admissible functions we have the bound -`∫ x in s t, B (u x) (f u x) ∂μ ≤ - β`. - -The most common choices for `B` are -- `inner ℝ`: passive -- `fun x y ↦ inner ℝ x y - δ • ‖x‖ ^ 2`: input strictly passive -- `fun x y ↦ inner ℝ x y - ε • ‖y‖ ^ 2`: output strictly passive -- `fun x y ↦ inner ℝ x y - δ • ‖x‖ ^ 2 - ε • ‖y‖ ^ 2`: very strictly passive -/ -def SetRel.IsDissipativeWith (f : SetRel (α → E) (α → F)) (β : ℝ) (P : (α → E) → (α → F) → Prop) - (μ : Measure α := by volume_tac) : Prop := - ∀ ⦃t⦄, MeasurableSet (s t) → ∀ ⦃u y⦄, P u y ∧ (u, y) ∈ f → ∫ x in s t, B (u x) (y x) ∂μ ≤ - β - -/-- A map `f` is dissipative with bound `β` if for all admissible functions we have the bound -`∫ x in s t, B (u x) (f u x) ∂μ ≤ - β`. - -The most common choices for `B` are -- `inner ℝ`: passive -- `fun x y ↦ inner ℝ x y - δ • ‖x‖ ^ 2`: input strictly passive -- `fun x y ↦ inner ℝ x y - ε • ‖y‖ ^ 2`: output strictly passive -- `fun x y ↦ inner ℝ x y - δ • ‖x‖ ^ 2 - ε • ‖y‖ ^ 2`: very strictly passive -/ -def Function.IsDissipativeWith (f : (α → E) → α → F) (β : ℝ) (P : (α → E) → Prop) - (μ : Measure α := by volume_tac) : Prop := - ∀ ⦃t⦄, MeasurableSet (s t) → ∀ ⦃u⦄, P u → ∫ x in s t, B (u x) (f u x) ∂μ ≤ - β - -variable [NormedAddCommGroup E] [NormedAddCommGroup F] diff --git a/DynamicalSystems/InputOutput/Passive.lean b/DynamicalSystems/InputOutput/Passive.lean new file mode 100644 index 0000000..7d344ff --- /dev/null +++ b/DynamicalSystems/InputOutput/Passive.lean @@ -0,0 +1,97 @@ +/- +Copyright (c) 2026 Moritz Doll. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Moritz Doll +-/ +module + +public import Mathlib.MeasureTheory.Function.LpSpace.Basic +public import Mathlib.MeasureTheory.Measure.Lebesgue.Basic +public import Mathlib.MeasureTheory.SpecificCodomains.Pi +public import DynamicalSystems.Mathlib.Analysis.ODE.GlobalExistence +public import DynamicalSystems.InputOutput.Causal + +/-! # Passive maps + +-/ + +public section + +open MeasureTheory Filter Bornology Set +open scoped NNReal ENNReal + +variable {ι α 𝕜 E F G : Type*} + +section definition + +variable [MeasurableSpace α] [TopologicalSpace α] [TopologicalSpace E] [TopologicalSpace F] + [ENorm E] [ENorm F] + +/-- A map `f` is passive with bound `β` if for all admissible functions we have the bound +`- ∫ x in s t, B (u x) (f u x) ∂μ ≤ β`. + +The most common choices for `B` are +- `inner ℝ`: passive +- `fun x y ↦ inner ℝ x y - δ • ‖x‖ ^ 2`: input strictly passive +- `fun x y ↦ inner ℝ x y - ε • ‖y‖ ^ 2`: output strictly passive +- `fun x y ↦ inner ℝ x y - δ • ‖x‖ ^ 2 - ε • ‖y‖ ^ 2`: very strictly passive -/ +def SetRel.IsPassiveWith (f : SetRel (α → E) (α → F)) (B : E → F → ℝ) (s : ι → Set α) (β : ℝ) + (p q : ℝ≥0∞) [p.HolderConjugate q] (μ : Measure α := by volume_tac) : Prop := + ∀ ⦃t u y⦄, MemLpLoc u p μ ∧ MemLpLoc y q μ ∧ (u, y) ∈ f → - ∫ x in s t, B (u x) (y x) ∂μ ≤ β + +/-- A map `f` is passive with bound `β` if for all admissible functions we have the bound +`- ∫ x in s t, B (u x) (f u x) ∂μ ≤ β`. + +The most common choices for `B` are +- `inner ℝ`: passive +- `fun x y ↦ inner ℝ x y - δ • ‖x‖ ^ 2`: input strictly passive +- `fun x y ↦ inner ℝ x y - ε • ‖y‖ ^ 2`: output strictly passive +- `fun x y ↦ inner ℝ x y - δ • ‖x‖ ^ 2 - ε • ‖y‖ ^ 2`: very strictly passive -/ +structure Function.IsPassiveWith (f : (α → E) → α → F) (B : E → F → ℝ) (s : ι → Set α) (β : ℝ) + (p q : ℝ≥0∞) [p.HolderConjugate q] (μ : Measure α := by volume_tac) : Prop where + memLpLoc : ∀ ⦃u⦄, MemLpLoc u p μ → MemLpLoc (f u) q μ + integral_le : + ∀ ⦃t u⦄, MemLpLoc u p μ → - ∫ x in s t, B (u x) (f u x) ∂μ ≤ β + +namespace Function.IsPassiveWith + +variable {f : (α → E) → α → F} {B B₁ B₂ : E → F → ℝ} {s : ι → Set α} {β β' : ℝ} {p q : ℝ≥0∞} + [p.HolderConjugate q] {μ : Measure α} + +theorem add_right + (hs : ∀ t, IsCompact (s t)) + (hB₁ : f.IsPassiveWith B₁ s β p q μ) + (hB₂ : f.IsPassiveWith B₂ s β' p q μ) + (hB₁' : ∀ (ν : Measure α) (u : α → E) (v : α → F), MemLp u p ν ∧ MemLp v q ν → Integrable (fun x ↦ B₁ (u x) (v x)) ν) : + f.IsPassiveWith (B₁ + B₂) s (β + β') p q μ := by + constructor + · intro u hu + apply hB₁.memLpLoc hu + · intro t u hu + calc + _ = -∫ (x : α) in s t, B₁ (u x) (f u x) ∂μ + (-∫ (x : α) in s t, B₂ (u x) (f u x) ∂μ) := by + simp only [Pi.add_apply] + rw [integral_add ?_ ?_] + · ring + · apply hB₁' (μ.restrict (s t)) u (f u) ⟨?_, ?_⟩ + · sorry + · sorry + · sorry + _ ≤ _ := by + gcongr + · apply hB₁.integral_le hu + · apply hB₂.integral_le hu + + +theorem graph_isPassiveWith (h : f.IsPassiveWith B s β p q μ) : + f.graph.IsPassiveWith B s β p q μ := by + intro t u y ⟨hu, hy, hf⟩ + simp only [mem_graph] at hf + rw [← hf] + exact h.integral_le hu + +end Function.IsPassiveWith + +end definition + +variable [NormedAddCommGroup E] [NormedAddCommGroup F] From 9a9d0ec683337e8c051f603af98f75eec4fff0c7 Mon Sep 17 00:00:00 2001 From: Moritz Doll Date: Wed, 29 Jul 2026 11:04:42 +1000 Subject: [PATCH 2/2] stuff --- DynamicalSystems/InputOutput/Passive.lean | 47 +++++++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/DynamicalSystems/InputOutput/Passive.lean b/DynamicalSystems/InputOutput/Passive.lean index 7d344ff..5e08289 100644 --- a/DynamicalSystems/InputOutput/Passive.lean +++ b/DynamicalSystems/InputOutput/Passive.lean @@ -22,6 +22,52 @@ open scoped NNReal ENNReal variable {ι α 𝕜 E F G : Type*} +section IsHolderMap + +section definition + +variable [NNNorm E] [NNNorm F] [NNNorm G] + +@[fun_prop] +def IsHolderMap (B : E → F → G) (p q : ℝ≥0∞) [p.HolderConjugate q] : Prop := + ∀ x y, ∃ C, ‖B x y‖₊ ≤ C * (‖x‖₊ * ‖y‖₊ + ‖x‖₊ ^ p.toReal + ‖y‖₊ ^ q.toReal) + +/- +Idea: proof integrability by writing +`B x y = B x y - C (‖x‖₊ ^ p.toReal + ‖y‖₊ ^ q.toReal) + C (..)` +the `(..)` part is dealt with by standard things and the first bit is `MemLp.of_bilin` +-/ + + +variable [MeasurableSpace α] + [TopologicalSpace E] [ENorm E] + [TopologicalSpace F] [ENorm F] + [TopologicalSpace G] [ContinuousENorm G] + +@[fun_prop] +def IsHolderMap (B : E → F → G) (p q : ℝ≥0∞) [p.HolderConjugate q] : Prop := + ∀ (ν : Measure α) (u : α → E) (v : α → F), MemLp u p ν ∧ MemLp v q ν → + Integrable (fun x ↦ B (u x) (v x)) ν + +#check MeasureTheory.eLpNorm'_le_eLpNorm'_mul_eLpNorm' +#check MemLp.of_bilin + +namespace IsHolderMap + +variable {B₁ B₂ : E → F → G} {p q : ℝ≥0∞} [p.HolderConjugate q] + +@[fun_prop] +theorem add [Add G] (hB₁ : IsHolderMap B₁ p q) (hB₁ : IsHolderMap B₂ p q) : + IsHolderMap (B₁ + B₂) p q := by + sorry + +end IsHolderMap + +end definition + +end IsHolderMap + + section definition variable [MeasurableSpace α] [TopologicalSpace α] [TopologicalSpace E] [TopologicalSpace F] @@ -58,6 +104,7 @@ namespace Function.IsPassiveWith variable {f : (α → E) → α → F} {B B₁ B₂ : E → F → ℝ} {s : ι → Set α} {β β' : ℝ} {p q : ℝ≥0∞} [p.HolderConjugate q] {μ : Measure α} + theorem add_right (hs : ∀ t, IsCompact (s t)) (hB₁ : f.IsPassiveWith B₁ s β p q μ)