SetRel.IsDissipativeWith.{u_1, u_2, u_4, u_5} {ι : Type u_1}
  {α : Type u_2} {E : Type u_4} {F : Type u_5} [MeasurableSpace α]
  (B : E → F → ℝ) {s : ι → Set α} (f : SetRel (α → E) (α → F)) (β : ℝ)
  (P : (α → E) → (α → F) → Prop)
  (μ : MeasureTheory.Measure α := by volume_tac) : Prop
SetRel.IsDissipativeWith.{u_1, u_2, u_4,
    u_5}
  {ι : Type u_1} {α : Type u_2}
  {E : Type u_4} {F : Type u_5}
  [MeasurableSpace α] (B : E → F → ℝ)
  {s : ι → Set α}
  (f : SetRel (α → E) (α → F)) (β : ℝ)
  (P : (α → E) → (α → F) → Prop)
  (μ : MeasureTheory.Measure α := by
    volume_tac) :
  Prop

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

Function.IsDissipativeWith.{u_1, u_2, u_4, u_5} {ι : Type u_1}
  {α : Type u_2} {E : Type u_4} {F : Type u_5} [MeasurableSpace α]
  (B : E → F → ℝ) {s : ι → Set α} (f : (α → E) → α → F) (β : ℝ)
  (P : (α → E) → Prop) (μ : MeasureTheory.Measure α := by volume_tac) :
  Prop
Function.IsDissipativeWith.{u_1, u_2, u_4,
    u_5}
  {ι : Type u_1} {α : Type u_2}
  {E : Type u_4} {F : Type u_5}
  [MeasurableSpace α] (B : E → F → ℝ)
  {s : ι → Set α} (f : (α → E) → α → F)
  (β : ℝ) (P : (α → E) → Prop)
  (μ : MeasureTheory.Measure α := by
    volume_tac) :
  Prop

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