Конструктивное доказательство

[Padawan]

Что такое конструктивное доказательство?
Можно ли считать доказательство теоремы Банаха-Штейнгауза конструктивным?
В такой формулировке:
Если последовательность непрерывных линейных операторов $A_n\colon X\to Y$ не ограничена по норме, то существует $x\in X$ такой, что $\sup_n\|A_nx\|=\infty$ ?

[_hum_]

если в ней описывается эффективный алгоритм нахождения того, что "существует", то, ИМХО, да.

[Padawan]

что значит эффективный алгоритм? Там при доказательстве строится последовательность вложенных шаров и берется их одноточечное пересечение.

-- Пн апр 09, 2012 16:18:21 --

Допустим $A_n$ -- это некоторые операторы в пространстве $C[a,b]$. И нам надо найти функцию $x(t)$, такую, что $\sup_{n} \|A_nx\|=\infty$. По доказательству теоремы Б.-Ш. можно для любого $\varepsilon>0$ указать непрерывную (даже кусочно-линейную) функцию $x_\varepsilon (t)$ такую, что $\|x_\varepsilon-x\|<\varepsilon$ для некоторой функции $x(t)$ c $\sup_{n} \|A_nx\|=\infty$.
Можно ли сказать, что эта функция $x(t)$ может быть эффективно построена?

Upd Чушь какая-то. Множество таких $x$ всюду плотно (его дополнение имеет первую категорию). Значит, в качестве $x_\varepsilon$ можно взять любую непрерывную функцию. Что же тогда понимать под эффективным построением?

[_hum_]

Эффективным обычно называют алгоритм, который всегда за конечное число шагов дает результат.
В вашем случае с этим не все очевидно, поскольку берется пересечение бесконечного числа шаров. Но возможно, если шары задаются конструктивно, то тут будет такая же ситуация, как и с конструктивными иррациональными числами. То есть, объекты, получаемые таким образом будут признаваться конструктивными.

[Padawan]

Наверное, само заключение теоремы должно быть эффективно проверяемым...

-- Пн апр 09, 2012 16:28:39 --

Можно ли считать конструктивным доказательством теоремы Б.-Ш. алгоритм, который выдает последовательность кусочно-линейных функций, равномерно сходящуюся к функции с нужным свойством?

[_hum_]

Вы бы точнее изложили, что вам нужно. Ибо под "конструктивным доказательством" может пониматься разное: начиная от неформального понимания конструктивности как явного построения, и оканчивая конструктивисткой математикой.

Padawan в сообщении #558295 писал(а):

Можно ли считать конструктивным доказательством теоремы Б.-Ш. алгоритм, который выдает последовательность кусочно-линейных функций, равномерно сходящуюся к функции с нужным свойством?

Очень похоже на то.

[ewert]

_hum_ в сообщении #558291 писал(а):

Эффективным обычно называют алгоритм, который всегда за конечное число шагов дает результат.

И такие алгоритмы образуют на множестве всех конструктивных алгоритмов подмножество меры ноль.

[Padawan]

ewert в сообщении #558542 писал(а):

_hum_ в сообщении #558291 писал(а):

Эффективным обычно называют алгоритм, который всегда за конечное число шагов дает результат.

И такие алгоритмы образуют на множестве всех конструктивных алгоритмов подмножество меры ноль.

Это образное выражение? Алгоритмов-то счетное множество.