ComponentPotential.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem356.ComponentPotential.glue line 17
Source documentation
Glue local potentials on disjoint components, with value zero outside them.
```
def glue (U : ι → Set E3) (u : ι → E3 → ℝ) (x : E3) : ℝ :=
…
```
Mentions: OAI.Problem356.E3
theorem OAI.Problem356.ComponentPotential.glue_eq line 20
theorem OAI.Problem356.ComponentPotential.glue_eq_zero line 33
theorem OAI.Problem356.ComponentPotential.measurable_glue line 44
Source documentation
Local continuity is sufficient for global Borel measurability of the extension.
```
theorem measurable_glue {U : ι → Set E3} {u : ι → E3 → ℝ}
    (hU : ∀ i, MeasurableSet (U i)) (hu : ∀ i, ContinuousOn (u i) (U i)) :
    Measurable (glue U u) := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.ComponentPotential.glue

theorem OAI.Problem356.ComponentPotential.continuousOn_glue line 55

Source documentation

Gluing preserves continuity on the open union of pairwise disjoint components.

theorem continuousOn_glue {U : ι → Set E3} {u : ι → E3 → ℝ}
    (hU : ∀ i, IsOpen (U i))
    (hdisj : Pairwise (fun i j => Disjoint (U i) (U j)))
    (hu : ∀ i, ContinuousOn (u i) (U i)) :
    ContinuousOn (glue U u) (⋃ i, U i) := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.ComponentPotential.glue

theorem OAI.Problem356.ComponentPotential.abs_glue_le line 67

Source documentation

A common absolute bound passes to the glued potential, globally if it is nonnegative.

theorem abs_glue_le {U : ι → Set E3} {u : ι → E3 → ℝ} {M : ℝ}
    (hM : 0 ≤ M) (hdisj : Pairwise (fun i j => Disjoint (U i) (U j)))
    (hu : ∀ i, ∀ x ∈ U i, |u i x| ≤ M) (x : E3) :
    |glue U u x| ≤ M := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.ComponentPotential.glue

theorem OAI.Problem356.ComponentPotential.integrable_glue line 79

Source documentation

A bounded glued potential is integrable against every finite marginal.

theorem integrable_glue {U : ι → Set E3} {u : ι → E3 → ℝ} {M : ℝ}
    {mu : Measure E3} [IsFiniteMeasure mu]
    (hM : 0 ≤ M) (hU : ∀ i, MeasurableSet (U i))
    (hdisj : Pairwise (fun i j => Disjoint (U i) (U j)))
    (hc : ∀ i, ContinuousOn (u i) (U i))
    (hb : ∀ i, ∀ x ∈ U i, |u i x| ≤ M) :
    Integrable (glue U u) mu := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.ComponentPotential.glue